/*
 * Alloy Analyzer
 * Copyright (c) 2004 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.gui;

import java.awt.BorderLayout;
import java.awt.Color;
import java.awt.Component;
import java.awt.Dimension;
import java.awt.Font;
import java.awt.FontMetrics;
import java.awt.Image;
import java.awt.Insets;
import java.awt.Rectangle;
import java.awt.Toolkit;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.awt.event.ComponentAdapter;
import java.awt.event.ComponentEvent;
import java.awt.event.ComponentListener;
import java.awt.event.HierarchyEvent;
import java.awt.event.HierarchyListener;
import java.awt.event.ItemEvent;
import java.awt.event.ItemListener;
import java.awt.event.KeyEvent;
import java.awt.event.WindowAdapter;
import java.awt.event.WindowEvent;
import java.awt.event.WindowListener;
import java.io.BufferedReader;
import java.io.ByteArrayOutputStream;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileOutputStream;
import java.io.FileReader;
import java.io.IOException;
import java.io.OutputStream;
import java.io.PrintStream;
import java.lang.reflect.Method;
import java.text.NumberFormat;
import java.util.ArrayList;
import java.util.Date;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.StringTokenizer;

import javax.swing.AbstractAction;
import javax.swing.Action;
import javax.swing.BorderFactory;
import javax.swing.Box;
import javax.swing.BoxLayout;
import javax.swing.ButtonGroup;
import javax.swing.ImageIcon;
import javax.swing.JButton;
import javax.swing.JCheckBox;
import javax.swing.JComboBox;
import javax.swing.JComponent;
import javax.swing.JDialog;
import javax.swing.JFrame;
import javax.swing.JLabel;
import javax.swing.JList;
import javax.swing.JMenu;
import javax.swing.JMenuBar;
import javax.swing.JMenuItem;
import javax.swing.JOptionPane;
import javax.swing.JPanel;
import javax.swing.JRadioButtonMenuItem;
import javax.swing.JScrollPane;
import javax.swing.JSplitPane;
import javax.swing.JTabbedPane;
import javax.swing.JTable;
import javax.swing.JTextArea;
import javax.swing.JTextField;
import javax.swing.JToolBar;
import javax.swing.KeyStroke;
import javax.swing.ListSelectionModel;
import javax.swing.UIManager;
import javax.swing.border.EmptyBorder;
import javax.swing.event.ListSelectionEvent;
import javax.swing.event.ListSelectionListener;
import javax.swing.plaf.basic.BasicComboBoxRenderer;
import javax.swing.table.AbstractTableModel;
import javax.swing.text.DefaultHighlighter;
import javax.swing.text.Highlighter;

import alloy.api.AlloyController;
import alloy.api.UnavailableOperationException;
import alloy.ast.Command;
import alloy.log.AlloyLog;
import alloy.log.LogPostAsker;
import alloy.util.BugPostAsker;
import alloy.util.CleanupManager;
import alloy.util.Dbg;
import alloy.util.ExtensionFileFilter;
import alloy.util.FileChooser;
import alloy.util.Msg;
import alloy.util.ParamEditor;
import alloy.util.ParamFormatException;
import alloy.util.ParameterEvent;
import alloy.util.ParameterListener;
import alloy.util.Params;
import alloy.viz.gui.VizPanel;

/**
 * @author Sam Daich
 * @author (modified by Robert Seater)
 */
public class NewAlloyGUI {

    /***** the tables *****/

    /** file table **/
    private final AlloyTable fileTable;
    private final FileTableModel fileTableModel;
    
    // column names
    private final String FT_MODE = "Mode";
    private final String FT_FILENAME = "Filename";
    private final String FT_LASTMODIFIED = "Last modified";

    /** analysis table **/
    private final AlloyTable analysisTable;
    private final AnalysisTableModel analysisTableModel;

    // column names
    private final String AT_TYPE = "+";
    private final String AT_NAME = "Name";
    private final String AT_FILENAME = "Filename";
    private final String AT_COMMAND = "Command";
    private final String AT_TIMESTARTED = "Time started";
    private final String AT_ELAPSEDTIME = "Elapsed time";

    /***** the layout panels *****/

    private final JFrame mainFrame = new AlloyWindow("Alloy Analyzer");;

    private JSplitPane verticalSplitPane;
    private JSplitPane horizontalSplitPane;

    // the detachable panels
    private final FileViewerPanel fileViewerPanel;
    private final InstanceViewerPanel instanceViewerPanel;
    private final AlloyPanel tablePanel;

    // the table panels
    private final JPanel filePanel;
    private final JScrollPane fileScrollPane;

    private final JPanel analysisPanel;
    private final JScrollPane analysisScrollPane;

    private final JPanel viewsPanel;

    // if the fileViewerPanel and instanceViewerPanel are both hidden,
    // this variable remembers the last size of the main window when
    // they weren't both hidden
    private Rectangle lastFullSizeBounds;
    
    // remembers the locations of the dividers    
    // the locations of the horizontal divider for when viz settings are 
    // displayed and when they're not are different.
    private int lastHorizontalSplitPaneDivider = -1;
    private int lastVizHorizontalSplitPaneDivider = -1;
    
    private int lastVerticalSplitPaneDivider = -1;

    /***** the state variables *****/

    /** List of all file windows */
    private final List filePanelList = new ArrayList(); // of ModelPanel

    /** Maps every open file to corresponding window.
	Thus, the map's values() set is a subset of filePanelList,
	but does not include windows corresponding to new unsaved files */
    private final Map filePanelMap = new HashMap(); // File -> ModelPanel

    /** the currently built file window */
    private ModelPanel builtFilePanel;

    /** the currently building file window */
    private ModelPanel buildingFilePanel;

    /** List of all analyses in table */
    private final List analysisList = new ArrayList(); // of Analysis

    /** These record the last things that may have marked up the text area, so we can wipe out those markings */
    private LiftedUnsatCoreHighlightVisitor _lastUcoreVisitor;
    private LocatableTextArea _lastErrorTextArea;
    //private alloy.ast.Location _lastErrorLocation; // Eclipse reports that this field is never read
    
    /***** globally accesible menu and toolbar components *****/

    // file menu
    private final JMenu fileMenu = new JMenu("File");

    // window menu
    private final JMenu windowMenu = AlloyWindow.makeWindowMenu("Window");

    private final JMenuItem reloadMenuItem = new JMenuItem("Reload", 'R');
    private final JMenuItem saveMenuItem = new JMenuItem("Save", 'S');
    private final JMenuItem saveAsMenuItem = new JMenuItem("Save As...", 'v');;
    private final JMenuItem saveCopyAsMenuItem = new JMenuItem("Save Copy As...", 'C');;
    private final JMenuItem closeMenuItem = new JMenuItem("Close", 'o');

    // edit menu
    private final JMenuItem undoMenuItem = new JMenuItem("Undo", 'U');
    private final JMenuItem redoMenuItem = new JMenuItem("Redo", 'R');
    private final JMenuItem cutMenuItem = new JMenuItem("Cut", 't');
    private final JMenuItem copyMenuItem = new JMenuItem("Copy", 'C');
    private final JMenuItem pasteMenuItem = new JMenuItem("Paste", 'P');
    private final JMenuItem deleteMenuItem = new JMenuItem("Delete", 'D');
;

    // view menu
    private OpenCloseMenuItem fileViewerMenuItem;
    private OpenCloseMenuItem instanceViewerMenuItem;
    private OpenCloseMenuItem tablesMenuItem;
    private final AlloySolutionMenuItem vizMenuItem = new AlloySolutionMenuItem(this, "Visualization", VIZ_MODE);
    private final AlloySolutionMenuItem consoleMenuItem = new AlloySolutionMenuItem(this, "Messages", CONSOLE_MODE);
    private final AlloySolutionMenuItem[] solutionMenuItems = {
        vizMenuItem,
        new AlloySolutionMenuItem(this, "Tree", TREE_MODE),
        new AlloySolutionMenuItem(this, "Tables", TABLE_MODE),
        new AlloySolutionMenuItem(this, "Text", TEXT_MODE),
        new AlloySolutionMenuItem(this, "XML", XML_MODE),
        new AlloySolutionMenuItem(this, "Dot", DOT_MODE),
        consoleMenuItem // not really a SolutionMenuItem, but uses the same code
    };

    // tools menu
    private final JMenuItem buildMenuItem = new JMenuItem("Build", 'B');
    private final JMenuItem executeMenuItem = new JMenuItem("Execute", 'E');
    private final JMenuItem removeHighlightsMenuItem = new JMenuItem("Remove Highlights", 'R');
    private final JMenuItem unsatCoreMenuItem = new JMenuItem("Unsat Core", 'U');
    private final JMenuItem metamodelMenuItem = new JMenuItem("Metamodel", 'M');
    private final JMenuItem nextMenuItem = new JMenuItem("Next", 'N');
    private final JMenuItem abortMenuItem = new JMenuItem("Abort", 'A');


    // general toolbar (new,open,save,prefs)
    private final JToolBar generalToolbar;

    private final JButton saveButton = new AlloyButton();

    // model toolbar
    private final JToolBar modelToolbar;

    private final JComboBox commandCombo = new JComboBox();
    private final JButton buildButton = new AlloyButton();
    private final JButton executeButton = new AlloyButton();
    private final JButton abortBuildButton = new AlloyButton();
    private final JButton abortExecuteButton = new AlloyButton();


    // views toolbar
    private final JToolBar viewsToolbar;

    // the vizButton is special, becuase it's also used for meta-models
    private final JButton vizButton = makeAlloySolutionButton("Viz", "Show Visualization", "images/24_graph.gif", VIZ_MODE);

    private final JButton[] solutionButtons = {
			vizButton,
			makeAlloySolutionButton("Tree", "Show Tree", "images/24_texttree.gif", TREE_MODE),
			makeAlloySolutionButton("Tables", "Show Tables", "images/24_texttree.gif", TABLE_MODE),
			makeAlloySolutionButton("Text", "Show Text", "images/24_plaintext.gif", TEXT_MODE),
			makeAlloySolutionButton("XML", "Show XML", "images/24_plaintext.gif", XML_MODE),
			makeAlloySolutionButton("Dot", "Show Dot", "images/24_plaintext.gif", DOT_MODE),
		};
    private JButton consoleButton;
    private JButton openSettingsButton;
    private JButton closeSettingsButton;
    private JButton updateSettingsButton;

    private int currentViewMode;
    private static final int VIZ_MODE = 0;
    private static final int TREE_MODE = 1;
    private static final int TEXT_MODE = 2;
    private static final int XML_MODE = 4;
    private static final int TABLE_MODE = 7;
    private static final int DOT_MODE = 5;
    private static final int CONSOLE_MODE = 3;

    // buttons for analysis toolbar
    private final JButton sourceButton = new AlloyButton();
    private final JButton evalButton = new AlloyButton();
    private final JButton deleteInstanceButton = new AlloyButton();
    private final JButton saveInstanceButton = new AlloyButton();
    
    // because parameter listeners are weakly referenced,
    // they cannot be local to a setup method.
    private ParameterListener textFontUpdater;
    private ParameterListener tableFontUpdater;
    private ParameterListener statusMsgsUpdater;
    private ParameterListener xmlAbbrevUpdater;

    /** variables used for the recent files menu **/
    private JMenu recentFilesMenu;

    // when recent files list is empty, use this
    private JMenuItem recentFilesEmptyMenuItem;

    // file where the list of recent files is saved
    private final File recentFilesFile = new File(".alloyrecentfiles"); 

    // max # files allowed in recent files menu
    private final int recentFilesMaxCount;

    // list of recent files
    private LinkedList recentFilesList;
    
    /* ****************************** */

    // the controller
    private AlloyController controller;

    // stream that prints to console
    private PrintStream consoleStream;

    private JPanel consolePanel;
    private final JTextArea consoleArea;

    private boolean isUpdatingFirstRow;

    // this listener is used for printing status messages
    private Dbg.DbgMsgStreamPrinter infoListener;

    private File rcFile; // current param file
    //private String workingDir; // current working directory
    private ExtensionFileFilter extFileFilter;
    private FileChooser chooser;
    private int analysisCount; // count for labelling untitled analyses

    private Box progressMsgBox;
    private JLabel progressMsgLabel;
    private JLabel progressMsgDash;

    private final NumberFormat leadingZerosFormat; // gives all integers at least 2 digits

    private static final String ALLOY_EXTENSION = "als";

    /**
     * constructor
     */
    public NewAlloyGUI() {
	// How do I get rid of the JTabbedPane borders???
	//UIManager.put("TabbedPane.contentBorderInsets",new Insets(0,0,0,0));

        /** intialize private variables */

		builtFilePanel = null;
		buildingFilePanel = null;

		recentFilesMaxCount = 10;
		initializeRecentFiles();

		isUpdatingFirstRow = false;

		rcFile = new File(System.getProperty("user.home"), "alloy.cfg");
		analysisCount = 1;

		extFileFilter = new ExtensionFileFilter(ALLOY_EXTENSION);
		chooser = new FileChooser(Params.glob.getParam("MAIN", "modeldir"));
		chooser.setFileFilter(extFileFilter);

		leadingZerosFormat = NumberFormat.getNumberInstance();
		leadingZerosFormat.setMinimumIntegerDigits(2);

		try {
			final boolean copyOK = Params.load(new FileInputStream(rcFile)).copyOnto(Params.glob);
			if (!copyOK)
				prefsWarning();
		} catch (IOException ex) {
			// do nothing
		} catch (ParamFormatException ex) {
			JOptionPane.showMessageDialog(mainFrame,
					"Error parsing preferences file.", "Default preferences",
					JOptionPane.ERROR_MESSAGE);
		}

		mainFrame.setIconImage(loadImage("images/32_logoicon.gif"));
		mainFrame.setJMenuBar(createMenuBar());
		mainFrame.setDefaultCloseOperation(JFrame.DO_NOTHING_ON_CLOSE);
		mainFrame.addWindowListener((WindowListener) AlloySwingUtilities.listener(new WindowAdapter() {
					public void windowClosing(WindowEvent e) {
						showQuitDialog();
					}
				}));

		BugPostAsker.setAsker(new GUIBugPostAsker());

		LogPostAsker.setAsker(new GUILogPostAsker());

		progressMsgLabel = new JLabel();
		// for some reason layout behaves strangely for minsize below (0,2)
		progressMsgLabel.setMinimumSize(new Dimension(0, 2));
		progressMsgDash = new JLabel();

		progressMsgBox = Box.createHorizontalBox();
		progressMsgBox.add(progressMsgDash);
		progressMsgBox.add(progressMsgLabel);
		progressMsgBox.add(Box.createHorizontalGlue());

		consolePanel = new JPanel(new BorderLayout());
		consoleArea = new JTextArea();
		consoleArea.setLineWrap(true);
		consoleArea.setWrapStyleWord(true);
		consoleArea.setEditable(true);
		consoleArea.setBackground(consolePanel.getBackground());
		consoleArea.setMargin(new Insets(0, 10, 0, 10));
		consoleArea.append("Welcome to Alloy Analyzer 3.0\n");
		consoleArea.setCaretPosition(consoleArea.getDocument().getLength());
		Font textFont = Params.glob.getFontParam("GUI", "textfont");
		consoleArea.setFont(textFont);

		consoleStream = new PrintStream(new OutputStream() {
			public void write(int b) {
				consoleArea.append(new String(new byte[] { (byte) b }));
				consoleArea.setCaretPosition(consoleArea.getDocument()
						.getLength());
			}
		});

		final JScrollPane consoleScrollPane = new JScrollPane(consoleArea);
		consoleScrollPane.setBorder(null);
		consolePanel.add(consoleScrollPane);

		infoListener = new Dbg.DbgMsgStreamPrinter(consoleStream);
		if (Params.glob.getBoolParam("MAIN", "statusMsgs"))
			Dbg.addDbgMsgListener(Dbg.INFO, infoListener);

		// warnings should always be printed
		Dbg.addDbgMsgListener(Dbg.WARN, infoListener);
		fileTableModel = new FileTableModel();
		analysisTableModel = new AnalysisTableModel();

		fileTable = new AlloyTable(fileTableModel);
		fileTable.getSelectionModel().addListSelectionListener(
				(ListSelectionListener) AlloySwingUtilities.listener(new ListSelectionListener() {
							public void valueChanged(ListSelectionEvent e) {
								fileViewerPanel.previewSelection();
								clearProgressMessage();
								updateAllMenuItems();
								updateCommandCombo();
							}
						}));
		fileTable.setColumnClipping(FT_FILENAME, AlloyTable.LEFT_CLIPPING);
		fileTable.setColumnIsFixedWidth(FT_MODE, true);

		analysisTable = new AlloyTable(analysisTableModel);
		analysisTable.setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION);
		analysisTable.getSelectionModel().addListSelectionListener(
				(ListSelectionListener) AlloySwingUtilities.listener(new ListSelectionListener() {
							public void valueChanged(ListSelectionEvent e) {
								instanceViewerPanel.previewSelection();
								updateAllMenuItems();
							}
						}));
		analysisTable.setColumnClipping(AT_FILENAME, AlloyTable.LEFT_CLIPPING);
		analysisTable.setColumnIsFixedWidth(AT_TYPE, true);
		analysisTable.hideColumn(AT_TIMESTARTED);
		analysisTable.setCanContinuouslyUpdateColumn(AT_ELAPSEDTIME, true);
		analysisTable.addHierarchyListener((HierarchyListener) AlloySwingUtilities.listener(new HierarchyListener() {
							public void hierarchyChanged(HierarchyEvent e) {
								continuouslyUpdateFirstAnalysisRow(isUpdatingFirstRow);
							}
						}));

		Font tableFont = Params.glob.getFontParam("GUI", "tablefont");
		fileTable.setFont(tableFont);
		analysisTable.setFont(tableFont);

		fileScrollPane = new JScrollPane(fileTable);
		analysisScrollPane = new JScrollPane(analysisTable);

		filePanel = new JPanel(new BorderLayout());
		filePanel.add(fileScrollPane, BorderLayout.CENTER);

		final JToolBar analysisToolbar = createAnalysisToolbar();
		analysisPanel = new JPanel(new BorderLayout());
		analysisPanel.add(analysisToolbar, BorderLayout.NORTH);
		analysisPanel.add(analysisScrollPane, BorderLayout.CENTER);

		viewsPanel = new JPanel(new BorderLayout());

		fileViewerPanel = new FileViewerPanel();
		fileViewerPanel.setSize(500, 500);
		fileViewerPanel.addAlloyPanelListener(new AlloyPanelAdapter() {
			public void alloyPanelHidden(AlloyPanelEvent e) {
				fileViewerMenuItem.showOpen();
			}

			public void alloyPanelShown(AlloyPanelEvent e) {
				fileViewerMenuItem.showClose();
			}
		});
		instanceViewerPanel = new InstanceViewerPanel();
		instanceViewerPanel.setSize(600, 400);
		instanceViewerPanel.addAlloyPanelListener(new AlloyPanelAdapter() {
			public void alloyPanelHidden(AlloyPanelEvent e) {
				instanceViewerMenuItem.showOpen();
			}

			public void alloyPanelShown(AlloyPanelEvent e) {
				instanceViewerMenuItem.showClose();
			}
		});

		final String defaultView = Params.glob.getParam("GUI", "defaultView");
		if (defaultView.equals("Visualization"))
			currentViewMode = VIZ_MODE;
		else if (defaultView.equals("Tree"))
			currentViewMode = TREE_MODE;
		else if (defaultView.equals("Text"))
			currentViewMode = TEXT_MODE;
		else if (defaultView.equals("XML"))
			currentViewMode = XML_MODE;
		else if (defaultView.equals("Tables"))
			currentViewMode = TABLE_MODE;
		else if (defaultView.equals("Dot"))
			currentViewMode = DOT_MODE;
		else {
			currentViewMode = VIZ_MODE;
			Dbg.warn("Unrecognized value (" + defaultView + ") for GUI.defaultView parameter");
		}

		final JTabbedPane tableTabbedPane = new JTabbedPane();
		tableTabbedPane.add("Files", filePanel);
		tableTabbedPane.add("Analyses", analysisPanel);
		tableTabbedPane.add("Views", viewsPanel);
		tablePanel = new AlloyPanel(tableTabbedPane, "<Tables>");
		tablePanel.addAlloyPanelListener(new AlloyPanelAdapter() {
			public void alloyPanelHidden(final AlloyPanelEvent e) {
				tablesMenuItem.showOpen();
			}
			public void alloyPanelShown(final AlloyPanelEvent e) {
				tablesMenuItem.showClose();
			}
		});

		final AlloyPanelListener panelArranger = new AlloyPanelAdapter() {
			public void alloyPanelHidden(final AlloyPanelEvent e) {
				// remember divider locations
				if (horizontalSplitPane != null)
					lastHorizontalSplitPaneDivider = horizontalSplitPane.getDividerLocation();
				if (verticalSplitPane != null)
					lastVerticalSplitPaneDivider = verticalSplitPane.getDividerLocation();
				if (e.getAlloyPanel().isAttached())
					arrangePanels();
			}

			public void alloyPanelShown(AlloyPanelEvent e) {
				if (e.getAlloyPanel().isAttached())
					arrangePanels();
			}

			public void alloyPanelAttached(AlloyPanelEvent e) {
				if (e.getAlloyPanel().isShown())
					arrangePanels();
			}

			public void alloyPanelDetached(AlloyPanelEvent e) {
				// remember divider locations
				if (horizontalSplitPane != null)
					lastHorizontalSplitPaneDivider = horizontalSplitPane.getDividerLocation();
				if (verticalSplitPane != null)
					lastVerticalSplitPaneDivider = verticalSplitPane.getDividerLocation();
				if (e.getAlloyPanel().isShown())
					arrangePanels();
			}
		};

		fileViewerPanel.addAlloyPanelListener(panelArranger);
		instanceViewerPanel.addAlloyPanelListener(panelArranger);
		tablePanel.addAlloyPanelListener(panelArranger);

		fileScrollPane.setMinimumSize(new Dimension(0, 0));
		fileScrollPane.setPreferredSize(new Dimension(300, 25));
		analysisScrollPane.setMinimumSize(new Dimension(0, 0));
		analysisScrollPane.setPreferredSize(new Dimension(300, 25));

		if (_onMac()) {
			fileTable.setBorder(null);
			analysisTable.setBorder(null);
			fileScrollPane.setBorder(new EmptyBorder(0, 0, 0, 0));
			analysisScrollPane.setBorder(new EmptyBorder(0, 0, 0, 0));
			filePanel.setBorder(null);
		}

		generalToolbar = createGeneralToolBar();
		modelToolbar = createModelToolBar();
		viewsToolbar = createViewsToolBar();

		setupParameterListeners();

		arrangePanels();
		mainFrame.pack(); // give all panels an initial size

		mainFrame
				.setSize(getScreenWidth() * 8 / 10, getScreenHeight() * 8 / 10);
		mainFrame.setLocation(getScreenWidth() / 10, getScreenHeight() / 10);

		if (!Params.glob.getBoolParam("GUI", "showTablesOnStartup"))
			tablePanel.makeHidden();

		arrangePanels();
		updateAllMenuItems();
		mainFrame.show();
	}

    /**
	 * @effect setup parameter listeners
	 */
    void setupParameterListeners() {
		textFontUpdater = new ParameterListener() {
			public void valueChanged(final ParameterEvent e) {
				Font textFont = Params.glob.getFontParam("GUI", "textfont");
				consoleArea.setFont(textFont);
			}
		};
		Params.glob.addParameterListener("GUI", "textfont", textFontUpdater);

		tableFontUpdater = new ParameterListener() {
			public void valueChanged(final ParameterEvent e) {
				Font tableFont = Params.glob.getFontParam("GUI", "tablefont");
				fileTable.setFont(tableFont);
				analysisTable.setFont(tableFont);
			}
		};
		Params.glob.addParameterListener("GUI", "tablefont", tableFontUpdater);

		statusMsgsUpdater = new ParameterListener() {
			public void valueChanged(final ParameterEvent e) {
				Dbg.removeDbgMsgListener(Dbg.INFO, infoListener);

				if (Params.glob.getBoolParam("MAIN", "statusMsgs"))
					Dbg.addDbgMsgListener(Dbg.INFO, infoListener);
			}
		};
		Params.glob.addParameterListener("MAIN", "statusMsgs",
				statusMsgsUpdater);

		xmlAbbrevUpdater = new ParameterListener() {
			public void valueChanged(final ParameterEvent e) {
				instanceViewerPanel.previewSelection();
			}
		};
		Params.glob.addParameterListener("MAIN", "xmlAbbrev", xmlAbbrevUpdater);
	}

    /**
     * @effect arrange panels
     */
    void arrangePanels() {
		final JComponent newArrange;
		final JComponent mainComponent;

		final boolean settingsShown = instanceViewerPanel.isSettingsPanelShown();
		final boolean includeFileViewer = fileViewerPanel.isShown() && fileViewerPanel.isAttached();
		final boolean includeInstanceViewer = instanceViewerPanel.isShown() && instanceViewerPanel.isAttached();
		final boolean includeTables = tablePanel.isShown() && tablePanel.isAttached();

		if (lastFullSizeBounds == null && !includeFileViewer && !includeInstanceViewer)
			lastFullSizeBounds = mainFrame.getBounds();

		if (lastFullSizeBounds != null && (includeFileViewer || includeInstanceViewer)) {
			mainFrame.setBounds(lastFullSizeBounds);
			lastFullSizeBounds = null;
		}

		mainFrame.getContentPane().removeAll();

		if (settingsShown) {
			final JPanel instanceArea = new JPanel(new BorderLayout());
			instanceArea.add(instanceViewerPanel, BorderLayout.CENTER);
			final Box instanceTopBox = Box.createHorizontalBox();
			instanceTopBox.add(viewsToolbar);
			//instanceTopBox.setPreferredSize(topBoxSize);
			instanceTopBox.setBorder(AlloySwingUtilities.createBottomBorder());
			instanceArea.add(instanceTopBox, BorderLayout.NORTH);

			if (horizontalSplitPane == null) {
				horizontalSplitPane = new AlloySplitPane(JSplitPane.HORIZONTAL_SPLIT);
				horizontalSplitPane.setResizeWeight(0.5);
				horizontalSplitPane.setContinuousLayout(true);
				horizontalSplitPane.setBorder(null);
			}

			// reset to last viz location
			if (lastVizHorizontalSplitPaneDivider > -1)
				horizontalSplitPane.setDividerLocation(lastVizHorizontalSplitPaneDivider);
			horizontalSplitPane.setLeftComponent(instanceViewerPanel.getSettingsPanel());
			horizontalSplitPane.setRightComponent(instanceArea);
			verticalSplitPane = null;
			mainComponent = horizontalSplitPane;
		} else if (includeFileViewer) {
			final JPanel fileArea = new JPanel(new BorderLayout());
			fileArea.add(fileViewerPanel, BorderLayout.CENTER);
			final Box fileTopBox = Box.createHorizontalBox();
			fileTopBox.add(generalToolbar);
			fileTopBox.add(modelToolbar);
			//fileTopBox.setPreferredSize(topBoxSize);
			fileTopBox.setBorder(AlloySwingUtilities.createBottomBorder());
			fileArea.add(fileTopBox, BorderLayout.NORTH);

			if (includeInstanceViewer) {
				final JPanel instanceArea = new JPanel(new BorderLayout());
				instanceArea.add(instanceViewerPanel, BorderLayout.CENTER);
				final Box instanceTopBox = Box.createHorizontalBox();
				instanceTopBox.add(viewsToolbar);
				//instanceTopBox.setPreferredSize(topBoxSize);
				instanceTopBox.setBorder(AlloySwingUtilities
						.createBottomBorder());
				instanceArea.add(instanceTopBox, BorderLayout.NORTH);

				if (includeTables) {
					if (verticalSplitPane == null) {
						verticalSplitPane = new AlloySplitPane(JSplitPane.VERTICAL_SPLIT);
						verticalSplitPane.setResizeWeight(0.7);
						verticalSplitPane.setContinuousLayout(true);
						verticalSplitPane.setBorder(null);
					}
					if (horizontalSplitPane == null) {
						horizontalSplitPane = new AlloySplitPane(JSplitPane.HORIZONTAL_SPLIT);
						horizontalSplitPane.setResizeWeight(0.5);
						horizontalSplitPane.setContinuousLayout(true);
						horizontalSplitPane.setBorder(null);
					}

					// reset divider location
					if (lastHorizontalSplitPaneDivider > -1)
						horizontalSplitPane.setDividerLocation(lastHorizontalSplitPaneDivider);
					if (lastVerticalSplitPaneDivider > -1)
						verticalSplitPane.setDividerLocation(lastVerticalSplitPaneDivider);

					verticalSplitPane.setTopComponent(instanceArea);
					verticalSplitPane.setBottomComponent(tablePanel);
					horizontalSplitPane.setLeftComponent(fileArea);
					horizontalSplitPane.setRightComponent(verticalSplitPane);
					mainComponent = horizontalSplitPane;
				} else { // not includeTables
					if (horizontalSplitPane == null) {
						horizontalSplitPane = new AlloySplitPane(JSplitPane.HORIZONTAL_SPLIT);
						horizontalSplitPane.setResizeWeight(0.5);
						horizontalSplitPane.setContinuousLayout(true);
						horizontalSplitPane.setBorder(null);
					}

					// reset divider location
					if (lastHorizontalSplitPaneDivider > -1)
						horizontalSplitPane.setDividerLocation(lastHorizontalSplitPaneDivider);
					horizontalSplitPane.setLeftComponent(fileArea);
					horizontalSplitPane.setRightComponent(instanceArea);

					verticalSplitPane = null;
					mainComponent = horizontalSplitPane;
				}
			} else { // not includeInstanceViewer
				if (includeTables) {
					if (verticalSplitPane == null) {
						verticalSplitPane = new AlloySplitPane(JSplitPane.VERTICAL_SPLIT);
						verticalSplitPane.setResizeWeight(0.7);
						verticalSplitPane.setContinuousLayout(true);
						verticalSplitPane.setBorder(null);
					}

					// reset divider location
					if (lastVerticalSplitPaneDivider > -1)
						verticalSplitPane.setDividerLocation(lastVerticalSplitPaneDivider);

					verticalSplitPane.setTopComponent(fileArea);
					verticalSplitPane.setBottomComponent(tablePanel);

					horizontalSplitPane = null;
					mainComponent = verticalSplitPane;
				} else { // not includeTables
					horizontalSplitPane = null;
					verticalSplitPane = null;
					mainComponent = fileArea;
				}
			}
		} else { // not includeFileViewer
			if (includeInstanceViewer) {
				final JPanel instanceArea = new JPanel(new BorderLayout());
				instanceArea.add(instanceViewerPanel, BorderLayout.CENTER);
				final Box instanceTopBox = Box.createHorizontalBox();
				instanceTopBox.add(generalToolbar);
				instanceTopBox.add(modelToolbar);
				instanceTopBox.add(viewsToolbar);
				//instanceTopBox.setPreferredSize(topBoxSize);
				instanceTopBox.setBorder(AlloySwingUtilities.createBottomBorder());
				instanceArea.add(instanceTopBox, BorderLayout.NORTH);

				if (includeTables) {
					if (verticalSplitPane == null) {
						verticalSplitPane = new AlloySplitPane(JSplitPane.VERTICAL_SPLIT);
						verticalSplitPane.setResizeWeight(0.7);
						verticalSplitPane.setContinuousLayout(true);
						verticalSplitPane.setBorder(null);
					}
					// reset divider location
					if (lastVerticalSplitPaneDivider > -1)
						verticalSplitPane.setDividerLocation(lastVerticalSplitPaneDivider);
					verticalSplitPane.setTopComponent(instanceArea);
					verticalSplitPane.setBottomComponent(tablePanel);
					horizontalSplitPane = null;
					mainComponent = verticalSplitPane;
				} else { // not includeTables
					horizontalSplitPane = null;
					verticalSplitPane = null;
					mainComponent = instanceArea;
				}
			} else { // not includeInstanceViewer
				if (includeTables) {
					JPanel tableArea = new JPanel(new BorderLayout());
					tableArea.add(tablePanel, BorderLayout.CENTER);
					Box tableTopBox = Box.createHorizontalBox();
					tableTopBox.add(generalToolbar);
					tableTopBox.add(modelToolbar);
					//tableTopBox.setPreferredSize(topBoxSize);
					tableTopBox.setBorder(AlloySwingUtilities.createBottomBorder());
					tableArea.add(tableTopBox, BorderLayout.NORTH);

					horizontalSplitPane = null;
					verticalSplitPane = null;
					mainComponent = tableArea;
				} else { // not includeTables
					horizontalSplitPane = null;
					verticalSplitPane = null;
					Box aloneBox = Box.createHorizontalBox();
					aloneBox.add(generalToolbar);
					aloneBox.add(modelToolbar);
					mainComponent = aloneBox;
				}
			}
		}

		newArrange = new JPanel(new BorderLayout());
		//if (mainComponent != null) {
		newArrange.add(mainComponent, BorderLayout.CENTER);
		//}
		//newArrange.add(toolbarPanel, BorderLayout.NORTH);

		mainFrame.getContentPane().add(newArrange);
		if (!includeFileViewer && !includeInstanceViewer) {
			tablePanel.setPreferredSize(tablePanel.getSize());
			mainFrame.pack();
			tablePanel.setPreferredSize(null);
		}
		mainFrame.validate();
	}

    /**
     * @param file
     */
	void addRecentFile(final File file) {
		if (recentFilesList.isEmpty())
			recentFilesMenu.removeAll();
		if (recentFilesList.contains(file)) {
			recentFilesMenu.remove(recentFilesList.indexOf(file));
			recentFilesList.remove(file);
		}
		while (recentFilesList.size() >= recentFilesMaxCount) {
			recentFilesMenu.remove(recentFilesList.size() - 1);
			recentFilesList.removeLast();
		}
		recentFilesList.addFirst(file);
		JMenuItem fileItem = new JMenuItem();
		fileItem.setAction(AlloySwingUtilities.action(new AbstractAction(file.getName()) {
			public void actionPerformed(final ActionEvent e) {
				createFilePanel(file, true);
				if (filePanelMap.containsKey(file))
					addRecentFile(file);
				else // the file cannot be opened
					removeRecentFile(file);
			}
		}));
		fileItem.setToolTipText(file.getPath());
		recentFilesMenu.add(fileItem, 0);
		writeRecentFiles();
	}

    /**
     * @param file
     */
	void removeRecentFile(final File file) {
		if (recentFilesList.contains(file)) {
			recentFilesMenu.remove(recentFilesList.indexOf(file));
			recentFilesList.remove(file);
		}
		if (recentFilesList.isEmpty())
			recentFilesMenu.add(recentFilesEmptyMenuItem);
		writeRecentFiles();
	}

    /**
	 * @effect write recent files
	 */
	void writeRecentFiles() {
		try {
			final PrintStream f = new PrintStream(new FileOutputStream(recentFilesFile));
			for (int i = recentFilesList.size() - 1; i >= 0; i--) {
				f.println(((File) recentFilesList.get(i)).getPath());
			}
		} catch (IOException ex) {
			Dbg.warn("could not write recent files file", ex);
		}
	}

    /**
     * @effect init recent files
     */
	void initializeRecentFiles() {
		recentFilesList = new LinkedList();
		recentFilesMenu = new JMenu();
		recentFilesEmptyMenuItem = new JMenuItem("<None>");
		recentFilesEmptyMenuItem.setEnabled(false);
		recentFilesMenu.add(recentFilesEmptyMenuItem);
		try {
			final BufferedReader reader = new BufferedReader(new FileReader(recentFilesFile));
			String line = reader.readLine();
			while (line != null && (recentFilesList.size() < recentFilesMaxCount)) {
				addRecentFile(new File(line));
				line = reader.readLine();
			}
		} catch (IOException ex) {
		}
	}

    /**
     * @effect clear progress message
     */
	void clearProgressMessage() {
		progressMsgDash.setText(null);
		progressMsgLabel.setText(null);
		progressMsgLabel.setToolTipText(null);
		progressMsgDash.repaint();
		progressMsgLabel.repaint();
	}

    /**
	 * @param message
	 */
	void sendProgressMessage(final String message) {
		progressMsgDash.setText(" - ");
		progressMsgLabel.setText(message);
		progressMsgLabel.setToolTipText(message);
		progressMsgDash.repaint();
		progressMsgLabel.repaint();

		consoleStream.println(message);
	}

    /**
     * @effect update all menu items
     */
    void updateAllMenuItems() {
	// refresh list of open files
	AlloyWindow.clearOpenFiles();

	Iterator i = filePanelList.iterator();
	while (i.hasNext()) {
			final ModelPanel filePanel = (ModelPanel) i.next();
			Action menuItemAction = AlloySwingUtilities.action(new AbstractAction(filePanel.getFileString()) {
						public void actionPerformed(ActionEvent e) {
							fileTable.setSelectedRowModelIndex(filePanelList.indexOf(filePanel));
						}
					});
			AlloyWindow.addOpenFileAction(menuItemAction);
		}

		boolean fileSelected = (fileTable.getSelectedRowCount() == 1);
		boolean fileViewerAttached = fileViewerPanel.isAttached();

		reloadMenuItem.setEnabled(fileSelected);
		saveMenuItem.setEnabled(fileSelected && getSelectedFilePanel().isEditable());
		saveButton.setEnabled(fileSelected && getSelectedFilePanel().isEditable());
		saveAsMenuItem.setEnabled(fileSelected);
		saveCopyAsMenuItem.setEnabled(fileSelected);
		closeMenuItem.setEnabled(fileSelected);

        undoMenuItem.setEnabled(fileSelected && fileViewerAttached && getSelectedFilePanel().isEditable());
        redoMenuItem.setEnabled(fileSelected && fileViewerAttached && getSelectedFilePanel().isEditable());
        cutMenuItem.setEnabled(fileSelected && fileViewerAttached && getSelectedFilePanel().isEditable());
        copyMenuItem.setEnabled(fileSelected && fileViewerAttached);
        pasteMenuItem.setEnabled(fileSelected && fileViewerAttached && getSelectedFilePanel().isEditable());
        deleteMenuItem.setEnabled(fileSelected && fileViewerAttached && getSelectedFilePanel().isEditable());

        if (fileSelected) {
			final ModelPanel selectedFilePanel = getSelectedFilePanel();

			final boolean isBuilt = (builtFilePanel == selectedFilePanel);
			final boolean isBuilding = (buildingFilePanel == selectedFilePanel);

			final boolean usePrimRel = false; //Params.glob.getBoolParam("MAIN", "primrel");

			final boolean enableBuild = controller == null || controller.isBuildAvailable();
			final boolean enableExecute = isBuilt && controller.isExecuteAvailable(usePrimRel);
			// how to determine when execution is finished?
			// abort doesn't work, so it is now disabled -- Derek 5 March 2005
			final boolean enableBuildAbortion = isBuilding && controller.isAbortAvailable();
			final boolean enableExecuteAbortion = isBuilt && controller.isAbortAvailable();

	    buildMenuItem.setEnabled(enableBuild);
	    buildButton.setEnabled(enableBuild);
	    buildButton.setVisible(!enableBuildAbortion);
	    abortBuildButton.setVisible(enableBuildAbortion);
	    executeMenuItem.setEnabled(enableExecute);
	    executeButton.setEnabled(enableExecute);
	    executeButton.setVisible(!enableExecuteAbortion);
	    unsatCoreMenuItem.setEnabled(isBuilt && controller.isUnsatCoreAvailable());
	    removeHighlightsMenuItem.setEnabled(true);
	    abortExecuteButton.setVisible(enableExecuteAbortion);
	    metamodelMenuItem.setEnabled(isBuilt && controller.isMetamodelAvailable());
	    nextMenuItem.setEnabled(isBuilt && controller.isNextAvailable());
	    abortMenuItem.setEnabled(enableBuildAbortion || enableExecuteAbortion);
        }
        else {
            buildMenuItem.setEnabled(false);
            buildButton.setEnabled(false);
            executeMenuItem.setEnabled(false);
            executeButton.setEnabled(false);
            unsatCoreMenuItem.setEnabled(false);
            removeHighlightsMenuItem.setEnabled(false);
            metamodelMenuItem.setEnabled(false);
            nextMenuItem.setEnabled(false);
            abortMenuItem.setEnabled(false);
        }

        // true if only one successful analysis is selected
        final boolean enableButtons =
        		analysisTable.getSelectedRowCount() == 1
			&& getSelectedAnalysis() instanceof SuccessfulAnalysis;
        evalButton.setEnabled(enableButtons);

        sourceButton.setEnabled(analysisTable.getSelectedRowCount() == 1);

        // This is separate from the other analysis buttons, because
        // it's possible to delete multiple analyses at once
        if (analysisTable.getSelectedRowCount() > 0 &&
	    !(analysisTable.getFirstRowIsTemp() &&
	      analysisTable.getSelectedRowCount() == 1 && 
	      analysisTable.getSelectedRow() == 0))
            deleteInstanceButton.setEnabled(true);
        else
            deleteInstanceButton.setEnabled(false);

	saveInstanceButton.setEnabled(analysisTable.getSelectedRow() == 0 &&
				      analysisTable.getFirstRowIsTemp() &&
				      !(analysisList.get(0) instanceof InProgressAnalysis));

	if (fileViewerPanel != null)
	    fileViewerPanel.updateMenuItems();

	updateViewModeButtons();
    }

    /**
     * @return the general tool bar
     */
    private JToolBar createGeneralToolBar() {
        JToolBar toolbar = new JToolBar();

        final JButton newButton = new AlloyButton();
		newButton.setAction(AlloySwingUtilities.action(new AbstractAction(
				"New", new ImageIcon(loadImage("images/24_new.gif"))) {
			public void actionPerformed(final ActionEvent e) {
				newFile();
			}
		}));
		newButton.setToolTipText("New File");
		toolbar.add(newButton);

        final JButton openButton = new AlloyButton();
		openButton.setAction(AlloySwingUtilities.action(new AbstractAction(
				"Open", new ImageIcon(loadImage("images/24_open.gif"))) {
			public void actionPerformed(final ActionEvent e) {
				openFile(true);
			}
		}));
		openButton.setToolTipText("Open File");
		toolbar.add(openButton);

		saveButton.setAction(AlloySwingUtilities.action(new AbstractAction(
				"Save", new ImageIcon(loadImage("images/24_save.gif"))) {
			public void actionPerformed(final ActionEvent e) {
				saveFile();
			}
		}));
		saveButton.setToolTipText("Save File");
		toolbar.add(saveButton);

        final JButton prefsButton = new AlloyButton();
		prefsButton.setAction(AlloySwingUtilities.action(new AbstractAction(
				"Prefs", new ImageIcon(loadImage("images/24_prefs.gif"))) {
			public void actionPerformed(final ActionEvent e) {
				_editOptions();
			}
		}));
		prefsButton.setToolTipText("Preferences");
		toolbar.add(prefsButton);

		toolbar.setFloatable(false);
		return toolbar;
    }

    /**
	 * @return the model tool bar
	 */
    private JToolBar createModelToolBar() {
        JToolBar toolbar = new JToolBar();

		commandCombo.setRenderer(new CommandCellRenderer(commandCombo));
		commandCombo.addItemListener((ItemListener) AlloySwingUtilities.listener(new ItemListener() {
					public void itemStateChanged(ItemEvent e) {
						if (commandCombo.getSelectedItem() != null
								&& controller != null
								&& getSelectedFilePanel() == builtFilePanel) {
							commandCombo.setToolTipText(stripAllQualifiers(commandCombo.getSelectedItem().toString()));
							try {
								controller.setCommand(commandCombo.getSelectedIndex() + 1);
							} catch (UnavailableOperationException ex) {
							}
						} else {
							commandCombo.setToolTipText(null);
						}
					}
				}));
		commandCombo.addComponentListener((ComponentListener) AlloySwingUtilities.listener(new ComponentAdapter() {
							public void componentResized(final ComponentEvent e) {
								commandCombo.validate();
							}
						}));
		toolbar.add(commandCombo);
		commandCombo.setMinimumSize(new Dimension(30, commandCombo.getPreferredSize().height));
		Dimension maxSize = commandCombo.getMaximumSize();
		maxSize.height = commandCombo.getPreferredSize().height;
		commandCombo.setMaximumSize(maxSize);
		updateCommandCombo();

		buildButton.setAction(AlloySwingUtilities.action(new AbstractAction(
				"Build", new ImageIcon(loadImage("images/24_build.gif"))) {
			public void actionPerformed(final ActionEvent e) {
				build(getSelectedFilePanel());
			}
		}));
		buildButton.setToolTipText("Build");

		abortBuildButton.setAction(AlloySwingUtilities.action(new AbstractAction(
				"Abort", new ImageIcon(loadImage("images/24_build_abort3.gif"))) {
					public void actionPerformed(final ActionEvent e) {
						abort();
					}
				}));
		abortBuildButton.setToolTipText("Abort Build");
		abortBuildButton.setVisible(false);

        toolbar.add(buildButton);
		toolbar.add(abortBuildButton);
		((AlloyButton) buildButton).setButtonForSizing((AlloyButton) abortBuildButton);

		executeButton.setAction(AlloySwingUtilities.action(new AbstractAction(
				"Execute", new ImageIcon(loadImage("images/24_execute.gif"))) {
			public void actionPerformed(final ActionEvent e) {
				execute(getSelectedFilePanel());
			}
		}));
		executeButton.setToolTipText("Execute");

		abortExecuteButton.setAction(AlloySwingUtilities
				.action(new AbstractAction("Abort", new ImageIcon(
						loadImage("images/24_execute_abort3.gif"))) {
					public void actionPerformed(final ActionEvent e) {
						abort();
					}
				}));
		abortExecuteButton.setToolTipText("Abort Execution");
		abortExecuteButton.setVisible(false);

		toolbar.add(executeButton);
		toolbar.add(abortExecuteButton);
		((AlloyButton) abortExecuteButton).setButtonForSizing((AlloyButton) executeButton);

		toolbar.setFloatable(false);
		return toolbar;
	}

    /**
	 * @author sam daich
	 */
    class CommandCellRenderer extends BasicComboBoxRenderer {
		JComboBox comboBox;

		CommandCellRenderer(JComboBox comboBox) {
			this.comboBox = comboBox;
		}

		public Component getListCellRendererComponent(
				JList list, Object value, int index, boolean isSelected, boolean cellHasFocus) {
			Object newValue;
			if (value instanceof Command.Info) {
				String text;
				final Command.Info commandInfo = (Command.Info) value; // ((Command) value).info();
				final FontMetrics fm = getFontMetrics(getFont());
				text = commandString(commandInfo, false);
				final Insets cInsets = comboBox.getInsets();
				final int cWidth = comboBox.getWidth() - (cInsets.left + cInsets.right);
				if (fm.stringWidth(text) > cWidth - 30)
					text = commandString(commandInfo, true);
				newValue = text;
				setToolTipText(stripAllQualifiers(commandInfo.toString()));
			} else {
				newValue = value;
				setToolTipText(null);
			}
			return super.getListCellRendererComponent(list, newValue, index, isSelected, cellHasFocus);
		}
	}

    /**
	 * update command combo
	 */
    private void updateCommandCombo() {
        int index = 0;
        if (controller != null)
            index = controller.getCommandIndex() - 1;

        commandCombo.removeAllItems();
        if (controller != null && getSelectedFilePanel() == builtFilePanel) {
            try {
                java.util.List commandInfoList = controller.allCommandInfos();
                for (int i = 0; i < commandInfoList.size(); i++) {
		    commandCombo.addItem(commandInfoList.get(i));
                }
                commandCombo.setSelectedIndex(index);
            }
            catch (UnavailableOperationException e) {
            }
        }
        else {
            commandCombo.addItem("Command Selection");
	    commandCombo.setToolTipText(null);
	}

    }

    /**
     * @param commandString
     * @return commandString without quantifiers
     */
    private static String stripAllQualifiers(final String commandString) {
		final ByteArrayOutputStream baos = new ByteArrayOutputStream();
		final PrintStream p = new PrintStream(baos);
		StringTokenizer st = new StringTokenizer(commandString, " \t\n\r\f,", true);
		while (st.hasMoreTokens())
			p.print(stripQualifiers(st.nextToken()));
		return baos.toString();
	}

    /**
	 * @param qName
	 * @return
	 */
    private static String stripQualifiers(final String qName) {
    		final StringTokenizer st = new StringTokenizer(qName, "/");
		String name = st.nextToken();
		while (st.hasMoreTokens())
			name = st.nextToken();
		return name;
	}

    /**
     * returns tersely formatted command, optionally with sigs abbreviated
     *
     * @param commandInfo
     * @param abbreviate
     * @return
     */
    private String commandString(final Command.Info commandInfo, final boolean abbreviate) {
	if (commandInfo.name != null)
	    return commandInfo.name;

	final ByteArrayOutputStream baos = new ByteArrayOutputStream();
	final PrintStream p = new PrintStream(baos);
	final ByteArrayOutputStream baosFull = new ByteArrayOutputStream();
	final PrintStream pFull = new PrintStream(baosFull);

	final StringTokenizer st = new StringTokenizer(commandInfo.toString(), " \t\n\r\f,");
	st.nextToken(); // "run" or "check"
	final String cmdType;
	if (commandInfo.isRunCommand()) {
	    cmdType = "run";
	} else if (commandInfo.isCheckCommand()) {
	    cmdType = "chk";
	} else {
	    cmdType = "???";
	    Dbg.warn("Unknown command type");
	}
	p.print(cmdType+" ");
	pFull.print(cmdType+" ");

	final String iden = st.nextToken();
	p.print(iden);
	pFull.print(iden);

	String token = st.hasMoreTokens() ? st.nextToken() : null;
	if (token != null && token.equals("for")) {
	    p.print(" [");
	    pFull.print(" [");

	    int scope;
	    String sig;

	    scope = Integer.parseInt(st.nextToken());
	    token = st.hasMoreTokens() ? st.nextToken() : null;
	    if (token != null && !token.equals("without") && !token.equals("expect")) {
				java.util.List scopeList = new ArrayList();
				java.util.List sigList = new ArrayList();
				sig = token;
				if (sig.equals("but")) {
					p.print(scope + ": ");
					pFull.print(scope + ": ");
					scope = Integer.parseInt(st.nextToken());
					sig = stripQualifiers(st.nextToken());
				} else {
					sig = stripQualifiers(sig);
				}
				scopeList.add(new Integer(scope));
				sigList.add(sig);
				token = st.hasMoreTokens() ? st.nextToken() : null;
				while (token != null && !token.equals("without") && !token.equals("expect")) {
					scope = Integer.parseInt(token);
					sig = stripQualifiers(st.nextToken());
					scopeList.add(new Integer(scope));
					sigList.add(sig);
					token = st.hasMoreTokens() ? st.nextToken() : null;
				}
				Trie t = new Trie();
				for (int i = 0; i < sigList.size(); i++) {
					t.add((String) sigList.get(i));
				}
				for (int i = 0; i < sigList.size(); i++) {
					String s = (String) sigList.get(i);
					String pre = t.minUniquePrefix(s);
					if (pre == null)
						pre = s;
					else if (pre.length() == 0)
						pre = s.substring(0, 1);

					p.print(scopeList.get(i) + " " + pre);
					if (i < sigList.size() - 1)
						p.print(", ");
					pFull.print(scopeList.get(i) + " " + s);
					if (i < sigList.size() - 1)
						pFull.print(", ");
				}
			} else {
				p.print(scope);
				pFull.print(scope);
			}
			p.print("]");
			pFull.print("]");
		}
		if (token != null && token.equals("without")) {
			String exclude = st.nextToken();
			p.print(" w/o " + exclude);
			pFull.print(" w/o " + exclude);
			token = st.hasMoreTokens() ? st.nextToken() : null;
			while (token != null && !token.equals("expect")) {
				p.print(", " + token);
				token = st.hasMoreTokens() ? st.nextToken() : null;
			}
		}
	if (token != null && token.equals("expect")) {
	    int n = Integer.parseInt(st.nextToken());
	    p.print(" (exp "+n+")");
	    pFull.print(" (exp "+n+")");
	}

	return abbreviate ? baos.toString() : baosFull.toString();
    }

    /**
     * @return the views tool bar
     */
    private JToolBar createViewsToolBar() {
		JToolBar toolbar = new JToolBar();

		openSettingsButton = new AlloyButton();
		openSettingsButton.setAction(AlloySwingUtilities
				.action(new AbstractAction("Layout", new ImageIcon(
						loadImage("images/24_settings.gif"))) {
					public void actionPerformed(final ActionEvent e) {
						instanceViewerPanel.showSettingsPanel();
						updateViewModeButtons();
					}
				}));
		openSettingsButton.setToolTipText("Open Layout Settings");
		toolbar.add(openSettingsButton);

		closeSettingsButton = new AlloyButton(AlloySwingUtilities
				.action(new AbstractAction("Close Layout", new ImageIcon(
						loadImage("images/24_settings_close2.gif"))) {
					public void actionPerformed(final ActionEvent e) {
						instanceViewerPanel.hideSettingsPanel();
						updateViewModeButtons();
					}
				}));
		closeSettingsButton.setToolTipText("Close Layout Settings");
		closeSettingsButton.setVisible(false);
		toolbar.add(closeSettingsButton);

		updateSettingsButton = new AlloyButton(AlloySwingUtilities
				.action(new AbstractAction("Update", new ImageIcon(
						loadImage("images/24_settings_apply2.gif"))) {
					public void actionPerformed(final ActionEvent e) {
						instanceViewerPanel.updateSettings();
					}
				}));
		updateSettingsButton.setToolTipText("Update");
		updateSettingsButton.setVisible(false);
		toolbar.add(updateSettingsButton);

		//put the different kinds of views after the layout buttons to prevent
		// the layout buttons from floating off of small screens

		for (int i = 0; i < solutionButtons.length; i++) {
			toolbar.add(solutionButtons[i]);
		}

		consoleButton = new AlloyButton();
		consoleButton.setAction(AlloySwingUtilities.action(new AbstractAction(
				"Msgs", new ImageIcon(loadImage("images/24_history.gif"))) {
			public void actionPerformed(final ActionEvent e) {
				setInstanceViewerMode(CONSOLE_MODE);
			}
		}));
		consoleButton.setToolTipText("Show Messages");
		toolbar.add(consoleButton);

		toolbar.setFloatable(false);
		updateViewModeButtons();

		return toolbar;
	}

    /**
     * @param mode
     */
    private void setInstanceViewerMode(final int mode) {
        AlloyLog.logStartSession(AlloyLog.VISUALIZATION);
        AlloyLog.logViz(AlloyLog.VISUALIZATION, mode);
		if (currentViewMode != mode) {
			currentViewMode = mode;
			updateViewModeButtons();
			instanceViewerPanel.previewSelection();
		}
        AlloyLog.logEndSession(AlloyLog.VISUALIZATION);
	}

    /**
	 * update view mode buttons
	 */
    private void updateViewModeButtons() {
		final boolean instanceShown = getSelectedAnalysis() instanceof SuccessfulAnalysis;
		final boolean metaShown = getSelectedAnalysis() instanceof SuccessfulMetaAnalysis;
		final boolean settingsShown = instanceViewerPanel.isSettingsPanelShown();

		// solutionMenuItems
		for (int i = 0; i < solutionMenuItems.length; i++) {
			solutionMenuItems[i].setSelected(currentViewMode);
			solutionMenuItems[i].setEnabled(instanceShown && !settingsShown);
		}
		// vizMenuItem and consoleMenuItem are special
		vizMenuItem.setEnabled((instanceShown || metaShown) && !settingsShown);
		consoleMenuItem.setEnabled((instanceShown || metaShown)
				&& !settingsShown);

		// regular solution buttons
		for (int i = 0; i < solutionButtons.length; i++) {
			solutionButtons[i].setEnabled(instanceShown && !settingsShown);
		}
		// the vizButton is special, so set it differently from other solBtns
		vizButton.setEnabled((instanceShown || metaShown) && !settingsShown);

		consoleButton.setEnabled((instanceShown || metaShown) && !settingsShown);
		openSettingsButton.setEnabled(currentViewMode == VIZ_MODE
				&& (instanceShown || metaShown) && !settingsShown);
		openSettingsButton.setVisible(!settingsShown);
		closeSettingsButton.setVisible(settingsShown);
		updateSettingsButton.setVisible(settingsShown);
	}

    /**
	 * @return the analysis tool bar
	 */
    private JToolBar createAnalysisToolbar() {
		JToolBar toolbar = new JToolBar();

		evalButton.setAction(AlloySwingUtilities.action(new AbstractAction("Eval",
				new ImageIcon(loadImage("images/24_evaluate.gif"))) {
			public void actionPerformed(final ActionEvent e) {
				((SuccessfulAnalysis) getSelectedAnalysis()).openEvalFrame();
			}
		}));
		evalButton.setToolTipText("Show Evaluator");
		toolbar.add(evalButton);

		sourceButton.setAction(AlloySwingUtilities.action(new AbstractAction("Source",
				new ImageIcon(loadImage("images/24_source.gif"))) {
			public void actionPerformed(final ActionEvent e) {
				getSelectedAnalysis().openModelFrame();
			}
		}));
		sourceButton.setToolTipText("Show Alloy Source");
		toolbar.add(sourceButton);

		deleteInstanceButton.setAction(AlloySwingUtilities.action(new AbstractAction("Delete",
				new ImageIcon(loadImage("images/24_trash.gif"))) {
					public void actionPerformed(final ActionEvent e) {
						deleteSelectedAnalyses();
					}
				}));
		deleteInstanceButton.setToolTipText("Delete Selected Instances");
		toolbar.add(deleteInstanceButton);

		saveInstanceButton.setAction(AlloySwingUtilities.action(new AbstractAction("Keep",
				new ImageIcon(loadImage("images/24_analysis.gif"))) {
					public void actionPerformed(final ActionEvent e) {
						analysisTable.setFirstRowIsTemp(false);
						analysisTableModel.fireTableRowsUpdated(0, 0);
						updateAllMenuItems();
					}
				}));
		saveInstanceButton.setToolTipText("Save Instance");
		toolbar.add(saveInstanceButton);
		toolbar.setFloatable(false);
		return toolbar;
	}

    /**
	 * @return the menu bar
	 */
    private JMenuBar createMenuBar() {
        JMenuBar mb;
        final int shortcutKeyMask = AlloySwingUtilities.getShortcutKeyMask();

        mb = new JMenuBar();

        // The file menu itself.
        fileMenu.setMnemonic('F');
        mb.add(fileMenu);

        // And now its contents.
        final JMenuItem newMenuItem = new JMenuItem("New", 'N');
        newMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("New") {
		public void actionPerformed(final ActionEvent e) {
		    newFile();
		}
	    }));
        newMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_N, shortcutKeyMask));
        fileMenu.add(newMenuItem);

        JMenuItem openMenuItem = new JMenuItem("Open", 'O');
        openMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Open") {
		public void actionPerformed(final ActionEvent e) {
		    openFile(true);
		}
	    }));
        openMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_O, shortcutKeyMask));
        fileMenu.add(openMenuItem);

	recentFilesMenu.setText("Open Recent");
	fileMenu.add(recentFilesMenu);

        JMenuItem openReadOnlyMenuItem = new JMenuItem("Open (Read-only)", 'p');
        openReadOnlyMenuItem
            .setAction(AlloySwingUtilities.action(new AbstractAction("Open (Read-only)") {
		    public void actionPerformed(final ActionEvent e) {
			openFile(false);
		    }
		}));
        openReadOnlyMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_P, shortcutKeyMask));
        fileMenu.add(openReadOnlyMenuItem);

        fileMenu.addSeparator();

        // And now its contents.
        reloadMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Reload") {
		public void actionPerformed(final ActionEvent e) {
		    reloadFile();
		}
	    }));
        reloadMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_L, shortcutKeyMask));
        fileMenu.add(reloadMenuItem);

        fileMenu.addSeparator();

        saveMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Save") {
		public void actionPerformed(final ActionEvent e) {
		    saveFile();
		    getSelectedFilePanel().getTextArea().requestFocus();
		}
	    }));
        saveMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_S, shortcutKeyMask));
        //saveMenuItem.setEnabled(isEditable());
        fileMenu.add(saveMenuItem);

        saveAsMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Save As...") {
		public void actionPerformed(final ActionEvent e) {
		    saveFileAs();
		}
	    }));
        fileMenu.add(saveAsMenuItem);

        saveCopyAsMenuItem
            .setAction(AlloySwingUtilities.action(new AbstractAction("Save Copy As...") {
		    public void actionPerformed(final ActionEvent e) {
			saveFileCopyAs();
		    }
		}));
        fileMenu.add(saveCopyAsMenuItem);

        if (!_onMac()) {
            fileMenu.addSeparator();

            JMenuItem editPrefsMenuItem = new JMenuItem("Preferences...", 'P');
            editPrefsMenuItem
                .setAction(AlloySwingUtilities.action(new AbstractAction("Preferences...") {
			public void actionPerformed(final ActionEvent e) {
			    _editOptions();
			}
		    }));
            fileMenu.add(editPrefsMenuItem);
        }
        fileMenu.addSeparator();

        closeMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Close") {
		public void actionPerformed(final ActionEvent e) {
		    closeFile();
		}
	    }));
        closeMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_W, shortcutKeyMask));
        fileMenu.add(closeMenuItem);
        fileMenu.addSeparator();

        JMenuItem quitMenuItem = new JMenuItem("Quit", 'Q');
        quitMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Quit") {
		public void actionPerformed(final ActionEvent e) {
		    showQuitDialog();
		}
	    }));
        quitMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_Q, shortcutKeyMask));
        fileMenu.add(quitMenuItem);

        final JMenu editMenu = new JMenu("Edit");
        editMenu.setMnemonic('E');
        mb.add(editMenu);

        undoMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Undo") {
		public void actionPerformed(final ActionEvent e) {
		    getSelectedFilePanel().getTextArea().undo();
		}
	    }));
        undoMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_Z, shortcutKeyMask));
        editMenu.add(undoMenuItem);

        redoMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Redo") {
		public void actionPerformed(final ActionEvent e) {
		    getSelectedFilePanel().getTextArea().redo();
		}
	    }));
        redoMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_R, shortcutKeyMask));
        editMenu.add(redoMenuItem);
        editMenu.addSeparator();

        cutMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Cut") {
		public void actionPerformed(final ActionEvent e) {
		    getSelectedFilePanel().getTextArea().cut();
		}
	    }));
        cutMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_X, shortcutKeyMask));
        editMenu.add(cutMenuItem);

        copyMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Copy") {
		public void actionPerformed(final ActionEvent e) {
		    getSelectedFilePanel().getTextArea().copy();
		}
	    }));
        copyMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_C, shortcutKeyMask));
        editMenu.add(copyMenuItem);

        pasteMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Paste") {
		public void actionPerformed(final ActionEvent e) {
		    getSelectedFilePanel().getTextArea().paste();
		}
	    }));
        pasteMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_V, shortcutKeyMask));
        editMenu.add(pasteMenuItem);

        deleteMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Delete") {
		public void actionPerformed(final ActionEvent e) {
		    getSelectedFilePanel().getTextArea().replaceSelection("");
		}
	    }));
        editMenu.add(deleteMenuItem);

        final JMenu viewsMenu = new JMenu("View");
        viewsMenu.setMnemonic('V');

        fileViewerMenuItem = new OpenCloseMenuItem(new AbstractAction("Show Editor") {
		public void actionPerformed(final ActionEvent e) {
                    AlloyLog.logStartSession(AlloyLog.SHOW_EDITOR);
		    fileViewerPanel.makeShown();
		    AlloyLog.logEndSession(AlloyLog.SHOW_EDITOR);
		}
	    }, new AbstractAction("Hide Editor") {
		    public void actionPerformed(final ActionEvent e) {
                        AlloyLog.logStartSession(AlloyLog.HIDE_EDITOR);
			fileViewerPanel.makeHidden();
			AlloyLog.logEndSession(AlloyLog.HIDE_EDITOR);
		    }
		}, false);
        viewsMenu.add(fileViewerMenuItem);

        instanceViewerMenuItem = new OpenCloseMenuItem(new AbstractAction("Show Output") {
		public void actionPerformed(final ActionEvent e) {
                    AlloyLog.logStartSession(AlloyLog.SHOW_OUTPUT);
		    instanceViewerPanel.makeShown();
		    AlloyLog.logEndSession(AlloyLog.SHOW_OUTPUT);
		}
	    }, new AbstractAction("Hide Output") {
		    public void actionPerformed(final ActionEvent e) {
                        AlloyLog.logStartSession(AlloyLog.HIDE_OUTPUT);
			instanceViewerPanel.makeHidden();
			AlloyLog.logEndSession(AlloyLog.HIDE_OUTPUT);
		    }
		}, false);
        viewsMenu.add(instanceViewerMenuItem);

        tablesMenuItem = new OpenCloseMenuItem(new AbstractAction("Show Tables") {
		public void actionPerformed(ActionEvent e) {
                    AlloyLog.logStartSession(AlloyLog.SHOW_TABLES);
		    tablePanel.makeShown();
		    AlloyLog.logEndSession(AlloyLog.SHOW_TABLES);
		}
	    }, new AbstractAction("Hide Tables") {
		    public void actionPerformed(final ActionEvent e) {
                        AlloyLog.logStartSession(AlloyLog.HIDE_TABLES);
			tablePanel.makeHidden();
			AlloyLog.logEndSession(AlloyLog.HIDE_TABLES);
		    }
		}, false);
        viewsMenu.add(tablesMenuItem);
	viewsMenu.addSeparator();

    { // restricted scope of bg
    	final ButtonGroup bg = new ButtonGroup();
    for (int i = 0; i < solutionMenuItems.length; i++) {
        bg.add( solutionMenuItems[i] );
        viewsMenu.add( solutionMenuItems[i] );
    }
    }
        mb.add(viewsMenu);

        final JMenu toolsMenu = new JMenu("Tools");
        toolsMenu.setMnemonic('T');

         buildMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Build") {
		public void actionPerformed(final ActionEvent e) {
		    build(getSelectedFilePanel());
		}
	    }));
        buildMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_B, shortcutKeyMask));
        toolsMenu.add(buildMenuItem);

        executeMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Execute") {
		public void actionPerformed(final ActionEvent e) {
		    execute(getSelectedFilePanel());
		}
	    }));
        executeMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_E, shortcutKeyMask));
        toolsMenu.add(executeMenuItem);

        //TODO shortcut key neither displays nor functions
	    removeHighlightsMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Remove Highlights") {
	    	public void actionPerformed(final ActionEvent e) {
	    		removeHighlights(getSelectedFilePanel());
	    	}
	    }));
	    removeHighlightsMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_R, shortcutKeyMask));
	    toolsMenu.add(removeHighlightsMenuItem);
        
         unsatCoreMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Unsat Core") {
		public void actionPerformed(final ActionEvent e) {
		    unsatCore(getSelectedFilePanel());
		}
	    }));
        unsatCoreMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_U, shortcutKeyMask));
        
	//
	// GREG: COMMENTING OUT UNSAT CORE FOR NOW!!
	// toolsMenu.add(unsatCoreMenuItem);
	//

        metamodelMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Metamodel") {
		public void actionPerformed(final ActionEvent e) {
		    metamodel(getSelectedFilePanel());
		}
	    }));
        toolsMenu.add(metamodelMenuItem);

        nextMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Next") {
		public void actionPerformed(final ActionEvent e) {
		    next(getSelectedFilePanel());
		}
	    }));
        nextMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_M, shortcutKeyMask));
        toolsMenu.add(nextMenuItem);

        abortMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Abort") {
		public void actionPerformed(final ActionEvent e) {
		    abort();
		}
	    }));
        abortMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_T, shortcutKeyMask));
        toolsMenu.add(abortMenuItem);
        mb.add(toolsMenu);

        windowMenu.setMnemonic('W');
        windowMenu.addSeparator();
        mb.add(windowMenu);


	//if (!_onMac()) {
	    JMenu helpMenu = new JMenu("Help");
	    helpMenu.setMnemonic('H');
	    mb.add(helpMenu);
	    
	    // user guide menu item
	    final JMenuItem userGuideMenuItem = new JMenuItem("User Guide");
	    userGuideMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("User Guide") {
	       public void actionPerformed(final ActionEvent e){
	           userGuide();
	       }
	    }));
	    helpMenu.add(userGuideMenuItem);
	    
	    helpMenu.addSeparator();
	    
	    JMenuItem aboutMenuItem = new JMenuItem("About Alloy Analyzer");
	    aboutMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("About Alloy Analyzer") {
		    public void actionPerformed(final ActionEvent e) {
			about();
		    }
		}));
	    helpMenu.add(aboutMenuItem);
	//}

    return mb;
    }

    /**
     * launch user guide
     */
    private void userGuide() {
    	AlloyLog.logStartSession(AlloyLog.USER_GUIDE);
        AlloyHelp.showHelp(mainFrame, AlloyHelp.HELP_DEFAULT);
        AlloyLog.logEndSession(AlloyLog.USER_GUIDE);
    }
    
    /**
     * used by alloy.gui.mac.MacUtils
     */
    public void about () {
	AlloySplashScreen.splash(mainFrame);
    }

    /**
     * @param e
     * @param isTemp
     */
    void addAnalysis(final Analysis e, final boolean isTemp) {
	if (analysisTable.getFirstRowIsTemp()) {
	    Analysis old = (Analysis)analysisList.set(0, e);
	    analysisTableModel.fireTableDataChanged();
	    analysisTable.setSelectedRowModelIndex(0);
	    old.releaseResources();
	} else {
	    analysisList.add(0, e);
	    analysisTableModel.fireTableRowsInserted(0,0);
	}
	analysisTable.setFirstRowIsTemp(isTemp);
	
	e.addAnalysisListener(new AnalysisListener() {
		public void nameChanged(AnalysisEvent e) {
		    instanceViewerPanel.previewSelection();
		}
	    });
	updateAllMenuItems();
    }

    /**
     * deselect
     */
    void deselectAllAnalyses() {
	if (analysisTable.getRowCount() > 0)
	    analysisTable.removeRowSelectionInterval(0, analysisTable.getRowCount()-1);
    }

    /**
     * delete selected analyses
     */
    void deleteSelectedAnalyses() {
        int[] indices = analysisTable.getSelectedRows();

        for (int i = analysisTable.getSelectedRowCount() - 1; i >= 0; i--) {
        	final int idx = indices[i];
	    if (!(idx == 0 && analysisTable.getFirstRowIsTemp())) {
	    	final Analysis old = (Analysis)analysisList.remove(idx);
		analysisTableModel.fireTableRowsDeleted(idx, idx);
		old.releaseResources();
	    }
        }
    }

    /**
     * @return
     */
    ModelPanel getSelectedFilePanel() {
        return (fileTable.getSelectedRowCount() == 1)
            ? (ModelPanel)filePanelList.get(fileTable.getSelectedRowModelIndex())
            : null;
    }

    /**
     * @return selected analysis
     */
    Analysis getSelectedAnalysis() {
        return (analysisTable.getSelectedRowCount() == 1)
            ? (Analysis)analysisList.get(analysisTable.getSelectedRowModelIndex())
            : null;
    }

    /**
     * create new model file
     */
    void newFile() {
    	AlloyLog.logStartSession(AlloyLog.NEW);
        createFilePanel(null, true);
        AlloyLog.logEndSession(AlloyLog.NEW);
    }

    /**
     * @param editable
     */
    void openFile(final boolean editable) {
        AlloyLog.logStartSession(editable == true ? AlloyLog.OPEN : AlloyLog.OPEN_READ_ONLY);
        if (chooser.showOpenDialog(mainFrame) == FileChooser.APPROVE_OPTION) {
        		final File selectedFile = chooser.getSelectedFile();
        		addRecentFile(selectedFile);
            createFilePanel(selectedFile, editable);
            if (editable == true) {
                AlloyLog.logFile(AlloyLog.OPEN, selectedFile.getAbsolutePath());
            } else {
                AlloyLog.logFile(AlloyLog.OPEN_READ_ONLY, selectedFile.getAbsolutePath());
            }
        }
        AlloyLog.logEndSession(editable == true ? AlloyLog.OPEN : AlloyLog.OPEN_READ_ONLY);
    }

    /**
     * reload
     */
    void reloadFile() {
    	AlloyLog.logStartSession(AlloyLog.RELOAD);
    	final ModelPanel modelPanel = getSelectedFilePanel();
	if (modelPanel.getTextArea().checkConfirmOperation()) {
	    modelPanel.getTextArea().reloadFile();
	    consoleStream.println("Reloading "+modelPanel.getTextArea().getFileName());

	    controller = null;
	    builtFilePanel = null;
	}
        AlloyLog.logEndSession(AlloyLog.RELOAD);
    }


    /**
     * save file without prompt
     */
    void saveFile() {
    	AlloyLog.logStartSession(AlloyLog.SAVE_FILE);
    	final ModelPanel modelPanel = getSelectedFilePanel();
	if (modelPanel.getFile() == null)
	    saveFileAs();
	else
	    modelPanel.getTextArea().saveFile();
	AlloyLog.logEndSession(AlloyLog.SAVE_FILE);
    }

    /**
     * save as
     */
    void saveFileAs() {
    	AlloyLog.logStartSession(AlloyLog.SAVE_FILE_AS);
    	final ModelPanel modelPanel = getSelectedFilePanel();
        if (chooser.showSaveDialog(mainFrame) == FileChooser.APPROVE_OPTION) {
        		final File selectedFile = extFileFilter.addExtensionIfNone(chooser.getSelectedFile());
        		modelPanel.getTextArea().saveFileAs(selectedFile);
        }
        AlloyLog.logEndSession(AlloyLog.SAVE_FILE_AS);
    }

    /**
     * save copy as
     */
    void saveFileCopyAs() {
    	AlloyLog.logStartSession(AlloyLog.SAVE_COPY_AS);
    	final ModelPanel modelPanel = getSelectedFilePanel();
        if (chooser.showSaveDialog(mainFrame) == FileChooser.APPROVE_OPTION) {
        		final File selectedFile = extFileFilter.addExtensionIfNone(chooser.getSelectedFile());
        		modelPanel.getTextArea().saveFileCopyAs(selectedFile);
        }
        AlloyLog.logEndSession(AlloyLog.SAVE_COPY_AS);
    }

    void closeFile() {
    	final ModelPanel modelPanel = getSelectedFilePanel();
	if ((builtFilePanel == modelPanel || buildingFilePanel == modelPanel)
	    && controller.isAbortAvailable()) {
	    JOptionPane.showMessageDialog(
					  mainFrame,
					  "Abort current operation before closing file",
					  "Error",
					  JOptionPane.ERROR_MESSAGE);
	    return;
	}

	if (modelPanel.getTextArea().checkConfirmOperation()) {
	    filePanelList.remove(modelPanel);
	    filePanelMap.values().remove(modelPanel);
	    if (builtFilePanel == modelPanel) {
	    		controller = null;
	    		builtFilePanel = null;
	    }

	    fileTableModel.fireTableDataChanged();
	    modelPanel.close();
	}
    }	

    /**
     * @param msgType_
     * @param msg_
     */
    void showError(final int msgType_, final Msg msg_) {
	alloy.ast.Node node = msg_.node;
	alloy.ast.Location location = node == null ? null : node.getLocation();
	final ModelPanel currentFilePanel = getSelectedFilePanel();
	ModelPanel errorFilePanel;

	//select the file that contains the error
	if (location == null ||
	    location.getFileName() == null ||
	    location.getFileName() == alloy.ast.Location.NOT_FROM_FILE) {
	    errorFilePanel = currentFilePanel;
	} else {
		final File errorFile = new File(location.getFileName()).getAbsoluteFile();
	    errorFilePanel = (ModelPanel)filePanelMap.get(errorFile);
	    if (errorFilePanel != currentFilePanel) {
		tablePanel.makeShown();
		// open errorFile if not open, and bring it to front
		createFilePanel(errorFile,currentFilePanel.isEditable());
		errorFilePanel = (ModelPanel)filePanelMap.get(errorFile);
		final GUIMsgListener errorFileGUIMsgListener = errorFilePanel.getGUIMsgListener();
		errorFileGUIMsgListener.clearErrors();
		errorFileGUIMsgListener.debugMsg(msgType_, msg_, null);
		errorFileGUIMsgListener.show();
	    }
	}
	//record this so we can wipe out the highlighting later
	//_lastErrorLocation = location; // this value is never used, so don't store it
	_lastErrorTextArea = errorFilePanel.getTextArea();
	//this highlights the error in the file
	final Color errorColor;
	if (Params.glob.getParam("GUI", "errorColor").equals("Orange")) {
		errorColor = new Color(255, 145, 65);
	} else if (Params.glob.getParam("GUI", "errorColor").equals("Pink")) {
		errorColor = new Color(255, 125, 170);
	} else if (Params.glob.getParam("GUI", "errorColor").equals("Blue")) {
		errorColor = new Color(100, 135, 255);
	} else if (Params.glob.getParam("GUI", "errorColor").equals("Yellow")) {
		errorColor = new Color(230, 210, 0);
	} else if (Params.glob.getParam("GUI", "errorColor").equals("Green")) {
		errorColor = new Color(0, 255, 0);
	} else {
		Dbg.info("That error color is not supported.  Using gray instead.");
		errorColor = new Color(200, 200, 200);
	}
	final Highlighter.HighlightPainter errorPainter =
		new DefaultHighlighter.DefaultHighlightPainter(errorColor);
	errorFilePanel.getTextArea().showLoc(location, errorPainter);

	java.awt.datatransfer.StringSelection selection =
	    new java.awt.datatransfer.StringSelection(msg_.toString());
	Toolkit.getDefaultToolkit().getSystemClipboard().setContents(selection, selection);
    }

    /**
     * @param file_
     * @param editable
     */
    void createFilePanel(final File file_, final boolean editable) {
	File file = file_ == null ? null : file_.getAbsoluteFile();
        ModelPanel textWindow;
        //JFrame replacedWindow = null;
        //boolean alreadyOpen = false;

        /*
        if (Params.glob.getBoolParam("GUI", "windowrepl")) {
			Iterator i = filePanelList.iterator();
			while (i.hasNext()) {
				JFrame frame = (JFrame) i.next();
				if (frame.isVisible()) {
					replacedWindow = frame;
					break;
				}
			}
		}
		*/
	
        if (filePanelMap.containsKey(file)) {
            textWindow = (ModelPanel)filePanelMap.get(file);
            if (textWindow.isEditable() != editable) {
                JOptionPane.showMessageDialog(
					      mainFrame,
					      "File is already open, but in "
					      + (editable ? "read-only" : "editable")
					      + " mode",
					      "Open file",
					      JOptionPane.WARNING_MESSAGE);
            }
	    fileTable.setSelectedRowModelIndex(filePanelList.indexOf(filePanelMap.get(file)));
        }
        else try {
            textWindow = new ModelPanel(file, editable);
            filePanelList.add(0, textWindow);
            fileTableModel.fireTableRowsInserted(0, 0);
            fileTable.setSelectedRowModelIndex(0);
            if (file != null)
                filePanelMap.put(file, textWindow);
            textWindow.setSize(500, 500);
	    textWindow.addModelPanelListener(new ModelPanelListener() {
		    public void modelChanged(ModelPanelEvent e) {
			ModelPanel modelPanel = e.getModelPanel();
			File modelFile = modelPanel.getFile();
			if (modelFile != null && filePanelMap.get(modelFile) != modelPanel) {
			    filePanelMap.values().remove(modelPanel);
			    filePanelMap.put(modelFile, modelPanel);
			}
			
			int rowIndex = filePanelList.indexOf(e.getModelPanel());
			fileTableModel.fireTableRowsUpdated(rowIndex, rowIndex);

			if (modelFile != null)
			    addRecentFile(modelFile);

			fileViewerPanel.previewSelection();
			if (!fileViewerPanel.isAttached())
			    fileViewerPanel.makeShown();
			updateAllMenuItems();
		    }
		    public void modelError(ModelPanelEvent e) {
			Object[] msgArray = (Object[])e.getMessage();
			int msgType_ = ((Integer)msgArray[0]).intValue();
			Msg msg_ = (Msg)msgArray[1];
			showError(msgType_, msg_);
		    }
		});
        } catch (IOException ex) {
	    return;
	}
        /*
	  if (editable || Params.glob.getBoolParam("GUI", "showreadonly")) {
	  if (replacedWindow == null) {
	  textWindow.showWindow();
	  } else
	  replaceWindow(textWindow, replacedWindow);
	  }
        */
        //textWindow.hideMsgPane();
    }

    /**
     * A method to create a new frame to show the AST of the current instance.
     */
    void showAST(final LocatableTextArea textArea_) {
	
	//new ASTViewer(controller.getLiftedUnsatCore(), controller.getLastTranslatedFormula(), textArea_);
    }

    	/**
    	 * stop logging, cleaup, quit
    	 */
    void quitProgram() {
        AlloyLog.logEndSession(AlloyLog.UI);
        CleanupManager.exit(0);

        // work-around for possible memory leak in Mac OS X Java 1.4.1
        mainFrame.remove(mainFrame.getJMenuBar());
    }

    /**
     * This method is public because it needs to be called from within alloy.gui.mac.MacUtils
     */
    public void showQuitDialog() {
        final Iterator i = filePanelList.iterator();
        while (i.hasNext()) {
            if (!((ModelPanel)i.next()).getTextArea().checkConfirmOperation())
                return;
        }
        quitProgram();
    }

    /**
     * the warning now actually saves the new params file
     */
    void prefsWarning() {
        final ParamEditor paramEditor = new ParamEditor(Params.glob);
        paramEditor.updateParams();
	
		try {
		    Params.glob.save(new FileOutputStream(rcFile));		    
		}
		catch (IOException ex) {
		    JOptionPane.showMessageDialog(
						  mainFrame,
						  "Failed to save the preferences file to " + 
						  rcFile.getAbsolutePath().toString(),
						  "Save preferences",
						  JOptionPane.ERROR_MESSAGE);

		}
	
    }

    /**
     * This method is public because it needs to be called from within alloy.gui.mac.MacUtils
     */
    public void _editOptions() {
        final ParamEditor paramEditor = new ParamEditor(Params.glob);
        final JButton loadButton = new JButton("Load...");
        final JButton saveButton = new JButton("Save");
        final JButton saveAsButton = new JButton("Save As...");
        final JButton okButton = new JButton("OK");
        final JButton cancelButton = new JButton("Cancel");
        final JPanel buttonPanel = new JPanel();
        buttonPanel.add(loadButton);
        buttonPanel.add(saveButton);
        buttonPanel.add(saveAsButton);
        buttonPanel.add(okButton);
        buttonPanel.add(cancelButton);

        final JDialog paramEditDialog = new JDialog(mainFrame, "Options", true /* modal */
						    );
        paramEditDialog.getRootPane().setDefaultButton(okButton);
        paramEditDialog.getContentPane().setLayout(new BorderLayout());
        paramEditDialog.getContentPane().add("North", paramEditor);
        paramEditDialog.getContentPane().add("South", buttonPanel);

        loadButton.addActionListener((ActionListener) AlloySwingUtilities.listener(new ActionListener() {
			public void actionPerformed(final ActionEvent e) {
				File selectedFile = null;

				final FileChooser chooser = new FileChooser(null);
				chooser.setSelectedFile(rcFile);

				if (chooser.showOpenDialog(mainFrame) == FileChooser.APPROVE_OPTION) {
					selectedFile = chooser.getSelectedFile();
					try {
						boolean copyOK = Params.load(
								new FileInputStream(selectedFile))
								.copyOnto(Params.glob);
						if (!copyOK)
							prefsWarning();
						paramEditor.updateEditor();
						//_refreshOptions();
					} catch (IOException ex) {
						JOptionPane.showMessageDialog(mainFrame,
								"Error reading file.",
								"Load preferences",
								JOptionPane.ERROR_MESSAGE);
					} catch (ParamFormatException ex) {
						JOptionPane.showMessageDialog(mainFrame,
								"Invalid preferences file.",
								"Load preferences",
								JOptionPane.ERROR_MESSAGE);
					}
				}
			}
		}));

        saveButton.addActionListener((ActionListener)AlloySwingUtilities.listener(new ActionListener() {
		    public void actionPerformed(final ActionEvent e) {
			paramEditor.updateParams();
			//_refreshOptions();

			try {
			    Params.glob.save(new FileOutputStream(rcFile));
			}
			catch (IOException ex) {
			    JOptionPane.showMessageDialog(
							  mainFrame,
							  "Error writing file.",
							  "Save preferences",
							  JOptionPane.ERROR_MESSAGE);
			}
		    }
		}));

        saveAsButton.addActionListener((ActionListener)AlloySwingUtilities.listener(new ActionListener() {
		    public void actionPerformed(ActionEvent e) {
			paramEditor.updateParams();
			//_refreshOptions();

			File selectedFile = null;

			FileChooser chooser = new FileChooser(null);
			chooser.setSelectedFile(rcFile);

			if (chooser.showSaveDialog(mainFrame) == FileChooser.APPROVE_OPTION) {
			    selectedFile = chooser.getSelectedFile();

			    try {
				Params.glob.save(new FileOutputStream(selectedFile));
				rcFile = selectedFile;
			    }
			    catch (IOException ex) {
				JOptionPane.showMessageDialog(
							      mainFrame,
							      "Error writing file.",
							      "Save preferences",
							      JOptionPane.ERROR_MESSAGE);

			    }
			}
		    }
		}));

        cancelButton.addActionListener((ActionListener)AlloySwingUtilities.listener(new ActionListener() {
		    public void actionPerformed(final ActionEvent e) {
				paramEditDialog.setVisible(false);
				paramEditor.restoreParams();
			}
		}));
        okButton.addActionListener((ActionListener)AlloySwingUtilities.listener(new ActionListener() {
		    public void actionPerformed(final ActionEvent e) {
			paramEditDialog.setVisible(false);
			paramEditor.updateParams();
			//_refreshOptions();
		    }
		}));

        paramEditDialog.pack();
		paramEditDialog.setLocation((getScreenWidth() - paramEditDialog.getWidth()) / 2,
				(getScreenHeight() - paramEditDialog.getHeight()) / 2);
		paramEditDialog.setVisible(true);
    }

    /**
     * it's not clear what this does, but apparently sam daich knew
     * @param b
     */
	void continuouslyUpdateFirstAnalysisRow(final boolean b) {
		isUpdatingFirstRow = b;
		analysisTable
				.continuouslyUpdateFirstRow(b && analysisTable.isShowing());
	}

    /**
     * @param textWindow panel containing the active model
     * @effect build (compile) the active model
     */
    void build(final ModelPanel textWindow) {
        // if the file is open as read only, we need to reload the file
        // in case the user is working with an external editor program
        if (!textWindow.isEditable())
            reloadFile();

        final LocatableTextArea textArea = textWindow.getTextArea();

        // removed save check when building, now saves automatically
        if (textArea.getFileName() != null /*&& textArea.checkConfirmOperation() == false*/)
        		saveFile();
	    		// return;

        textWindow.getGUIMsgListener().clearErrors();

        // start receiving compiler error messages
        textWindow.getGUIMsgListener().dbgRegister();

        builtFilePanel = null;
        int commandIndex = controller == null ? -1 : controller.getCommandIndex();

        try {
            if (textArea.getFilePath() == null) {
                controller = new AlloyController(textArea.getText());
            }
            else {
                controller = new AlloyController(new File(textArea.getFilePath()));
            }
            // these two lines used to be after the build, but should be before it
            sendProgressMessage("Compiling " + textWindow.getFileString() + " ...");
            deselectAllAnalyses();
     		// reduce peak memory consumption by putting a dummy row in the analysis table
     		// so that the table doesn't hold onto an unnecessary old solution
            addAnalysis(new NullAnalysis(textWindow), true);
            // do the build
            controller.build(buildFinisher(textWindow, commandIndex));
            buildingFilePanel = textWindow;
            updateAllMenuItems();
        }
        catch (UnavailableOperationException ex) {
            unavailableOperation();
        }
        catch (IOException ex) {
            JOptionPane.showMessageDialog(
					  textWindow,
					  "File does not exist: " + textArea.getFilePath(),
					  "Build",
					  JOptionPane.ERROR_MESSAGE);
        }
    }

    /**
     * @param textWindow
     */
    void metamodel(final ModelPanel textWindow) {
    	AlloyLog.logStartSession(AlloyLog.METAMODEL);
        final LocatableTextArea textArea = textWindow.getTextArea();

        if (textArea.getFileName() != null && textArea.checkConfirmOperation() == false)
            return;

        final String workLabDisp = "Generating metamodel...";
        sendProgressMessage(workLabDisp);

	continuouslyUpdateFirstAnalysisRow(true);

        Date currentTime = new Date(System.currentTimeMillis());

        try {
            controller.metamodel(
				 metamodelFinisher(
						   textWindow,
						   textWindow.getTextArea().getText(),
						   controller.getCommandInfo(),
						   currentTime));
        }
        catch (UnavailableOperationException e1) {
            Dbg.fatal("Problem generating metamodel", e1);
        }
        
        String name = "metamodel";
	    name = name + "_" + leadingZerosFormat.format(analysisCount);

        addAnalysis(new InProgressMetaAnalysis(name,
					       textWindow,
					       textWindow.getTextArea().getText(),
					       null,
					       currentTime),
		    true);

        updateAllMenuItems();

        AlloyLog.logEndSession(AlloyLog.METAMODEL);
    }
    
    /**
     * analyze the selected command
     * @param textWindow
     */
    void execute(final ModelPanel textWindow) {
        LocatableTextArea textArea = textWindow.getTextArea();

        if (textArea.getFileName() != null && textArea.checkConfirmOperation() == false)
            return;

        try {
            Date currentTime;

	    /*
            if (Params.glob.getBoolParam("MAIN", "primrel")) {
                Set primVars = _specifyPrimaryRelations(controller.getCommandData());
		if (primVars == null) // cancelled by user
		    return;

		continuouslyUpdateFirstAnalysisRow(true);
		currentTime = new Date(System.currentTimeMillis());
                controller.execute(
				   primVars,
				   solveFinisher(
						 textWindow,
						 textWindow.getTextArea().getText(),
						 controller.getCommand(),
						 currentTime));
            }
            else {
	    */
	    continuouslyUpdateFirstAnalysisRow(true);
	    currentTime = new Date(System.currentTimeMillis());
	    controller.execute(
			       solveFinisher(
					     textWindow,
					     textWindow.getTextArea().getText(),
					     controller.getCommandInfo(),
					     currentTime));
	    //}

            addAnalysis(new InProgressAnalysis("",
					       textWindow,
					       textWindow.getTextArea().getText(),
					       controller.getCommandInfo(),
					       currentTime),
			true);

            final String workLabDisp = "Executing command " + controller.getCommandInfo().toString() + "...";
            sendProgressMessage(workLabDisp);

            updateAllMenuItems();
        }
        catch (UnavailableOperationException ex) {
            unavailableOperation();
        }
    }

    /**
     * called when removeHighlightsMenuItem is selected
     * 
     * @param textWindow the window from which ucore/error paintings should be removed
     */
    void removeHighlights(final ModelPanel textWindow) {
    		//Dbg.info("Removing highlights...");
    		sendProgressMessage("Removing highlights from " + textWindow.getFileString() + ".");
    		if(_lastUcoreVisitor != null)
    			_lastUcoreVisitor.hideLiftedUnsatCore();
    		
    		//wipe out error message markings
    		if(_lastErrorTextArea != null) {
    			_lastErrorTextArea.clearLocs();
        		textWindow.getGUIMsgListener().clearErrors();
   		}
    }
    
    /**
     * called when unsatCoreMenuItem is selected
     * 
     * @param textWindow
     */
    void unsatCore(final ModelPanel textWindow) {
        AlloyLog.logStartSession(AlloyLog.UNSAT);
    		final LocatableTextArea textArea = textWindow.getTextArea();

        if (textArea.getFileName() != null && textArea.checkConfirmOperation() == false)
            return;

        try {
	    // what does this do?
	    continuouslyUpdateFirstAnalysisRow(true);

            Date currentTime = new Date(System.currentTimeMillis());

	    // calls AlloyController code
            controller.unsatCore(
			    unsatCoreFinisher(
					  textWindow,
					  textWindow.getTextArea().getText(),
					  controller.getCommandInfo(),
					  currentTime));

			// get the name of the command
			StringTokenizer st = new StringTokenizer(controller.getCommandInfo().toString());
			st.nextToken();
			final String commandName = st.nextToken();
			
			String name = "unsatCore";
			name = commandName + "_" + name + "_" + leadingZerosFormat.format(analysisCount);
			
            addAnalysis(new InProgressAnalysis(name,
					       textWindow,
					       textWindow.getTextArea().getText(),
					       controller.getCommandInfo(),
					       currentTime),
			true);

            final String workLabDisp = "Computing unsatisfiable core...";
            sendProgressMessage(workLabDisp);
            updateAllMenuItems();
        }
        catch (UnavailableOperationException ex) {
            unavailableOperation();
        }
        AlloyLog.logEndSession(AlloyLog.UNSAT);
    }

    /**
     * generates the next solution
     * only works if mchaff is selected (or another solver capable of enumeration)
     * @param textWindow
     */
    void next(final ModelPanel textWindow) {
    	AlloyLog.logStartSession(AlloyLog.NEXT);
        final LocatableTextArea textArea = textWindow.getTextArea();

        if (textArea.getFileName() != null && textArea.checkConfirmOperation() == false)
            return;

        try {
	    continuouslyUpdateFirstAnalysisRow(true);

            final Date currentTime = new Date(System.currentTimeMillis());

            controller.next(
			    solveFinisher(
					  textWindow,
					  textWindow.getTextArea().getText(),
					  controller.getCommandInfo(),
					  currentTime));

            addAnalysis(new InProgressAnalysis("",
					       textWindow,
					       textWindow.getTextArea().getText(),
					       controller.getCommandInfo(),
					       currentTime),
			true);

            final String workLabDisp = "Executing command " + controller.getCommandInfo().toString() + "...";
            sendProgressMessage(workLabDisp);
            updateAllMenuItems();
        }
        catch (UnavailableOperationException ex) {
            unavailableOperation();
        }
        AlloyLog.logEndSession(AlloyLog.NEXT);
    }

    /**
     * @param textWindow
     * @param lastSelectedCommandIndex
     * @return
     */
    AlloyController.ThreadFinisher buildFinisher(final ModelPanel textWindow,
						 final int lastSelectedCommandIndex) {
        return new AlloyController.ThreadFinisher() {
		public void threadFinished(final Object success) {
		    AlloySwingUtilities.invokeLater(new Runnable() {
			    public void run() {
				GUIMsgListener msgListener = textWindow.getGUIMsgListener();
				LocatableTextArea textArea = textWindow.getTextArea();

				final boolean compileOk = ((Boolean)success).booleanValue();

				//Dbg.chk(compileOk || msgListener.hasErrors(), "compileOk");

				if (msgListener.hasErrors()) {
				    msgListener.show();
				}
				else {
				    msgListener.hide();
				    textArea.showLoc(null);
				}

				buildingFilePanel = null;

				if (compileOk) {
				    builtFilePanel = textWindow;
				    //nameUnnamedCommands(controller);
				    try {
					if (lastSelectedCommandIndex > 0 &&
					    lastSelectedCommandIndex <= controller.numCommands())
					    controller.setCommand(lastSelectedCommandIndex);
				    } catch (UnavailableOperationException ex) {}
				}

				// stop receiving compiler error messages
				textWindow.getGUIMsgListener().dbgDeregister();

				// make sure old command cell is gone
				//if (fileTable.isEditing())
				//    fileTable.getCellEditor().stopCellEditing();
				//fileTableModel.fireTableDataChanged();
				updateAllMenuItems();

				if (!compileOk) {
				    if (controller.lastRunAborted()) {
				    		sendProgressMessage("Compilation aborted.");
				    } else {
				    		sendProgressMessage("There were compile errors.");
				    }
				}
				else {
				    sendProgressMessage("Compilation successful.");
				}

				updateCommandCombo();
				//int windowIndex = filePanelList.indexOf(textWindow);
				//fileTable.setSelectedRowModelIndex(windowIndex);
			    }
			});
		}
	    };
    }

    /**
     * @param textWindow
     * @param modelString
     * @param commandInfo
     * @param startTime
     * @return
     */
    AlloyController.ThreadFinisher unsatCoreFinisher(final ModelPanel textWindow,
						     final String modelString,
						     final Command.Info commandInfo,
						     final Date startTime) {
	return new AlloyController.ThreadFinisher() {
		public void threadFinished(final Object success) {
		    final long durationMillis = System.currentTimeMillis() - startTime.getTime();
		    
		    AlloySwingUtilities.invokeLater(new Runnable() {
			    public void run() {
				final boolean unsatCoreOK = ((Boolean)success).booleanValue();
				
				// not sure what this does -edmond
				continuouslyUpdateFirstAnalysisRow(false);

				// get the name of the command
				final StringTokenizer st = new StringTokenizer(commandInfo.toString());
				st.nextToken();
				final String commandName = st.nextToken();

				if (unsatCoreOK) {
				    String name = "unsatCore";
				    name = commandName + "_" + name + "_" + leadingZerosFormat.format(analysisCount++);
				    
				    // contruct the unsat core visitor and traverse the formula tree
				    LiftedUnsatCoreHighlightVisitor unsatCoreVisitor = 
				    		LiftedUnsatCoreHighlightVisitor.constructVisitor(
				    			controller.getLiftedUnsatCore(),
				    			controller.getLastTranslatedFormula());
				    
				    // open up all the files that were referenced by the current file
				    // and map to their fileNames to their text areas
				    final Set fileNames = unsatCoreVisitor.getFileNames();
				    if (fileNames.size() > 1) {
				    		tablePanel.makeShown();	
				    		//fileViewerPanel.makeShown();
				    }

				    for (Iterator i = fileNames.iterator(); i.hasNext();) {
				    		final String fileName = (String)i.next();
				    		final File file = new File(fileName).getAbsoluteFile();
				    		ModelPanel panel = (ModelPanel)filePanelMap.get(file);
				    		if (panel == null) {
				    			createFilePanel(file, true);
				    			panel = (ModelPanel)filePanelMap.get(file);
				    		}
				    		unsatCoreVisitor.mapFileToTextArea(fileName, panel.getTextArea()); 					
				    }
				    
				    // set top file back to original file
				    fileTable.setSelectedRowModelIndex(filePanelList.indexOf(textWindow));
				    
				    addAnalysis(new SuccessfulUnsatCoreAnalysis(name,
															textWindow,
															modelString,
															commandInfo,
															startTime,
															durationMillis,
															// send an unsat core visitor instead?
															unsatCoreVisitor),
						true);  
				    showAST(textWindow.getTextArea());
				    sendProgressMessage("Unsatisfiable core computed. (" + new Time(durationMillis) + ")");

				    // Idea:
				    // preview selection - visualizes unsat core
				    // this run() method builds the tree
				} else {
				    String name = "unsatCoreAborted";
				    name = commandName + "_" + name + "_" + leadingZerosFormat.format(analysisCount++);
				    addAnalysis(new FailedAnalysis(name,
								   textWindow,
								   modelString,
								   commandInfo,
								   startTime,
								   durationMillis),
						true);
				    sendProgressMessage("Unsatisfiable core computation aborted.");
				}
			    }
		       
			});
		}
	    };
    }		     

    /**
     * copied from solveFinisher...not everything in here might be necessary
     * 
     * @param textWindow
     * @param modelString
     * @param commandInfo
     * @param startTime
     * @return
     */
    AlloyController.ThreadFinisher metamodelFinisher(
						     final ModelPanel textWindow,
						     final String modelString,
						     final Command.Info commandInfo,
						     final Date startTime) {
        return new AlloyController.ThreadFinisher() {
		public void threadFinished(final Object success) {
		    final long durationMillis = System.currentTimeMillis() - startTime.getTime();

		    AlloySwingUtilities.invokeLater(new Runnable() {
			    public void run() {
				boolean solveOk = ((Boolean)success).booleanValue();

				continuouslyUpdateFirstAnalysisRow(false);

				if (solveOk) {
				    String name = "metamodel";
				    name = name + "_" + leadingZerosFormat.format(analysisCount++);
				    addAnalysis(new SuccessfulMetaAnalysis(name,
									   textWindow,
									   modelString,
									   commandInfo,
									   startTime,
									   durationMillis,
									   controller.getMetaInstance()),
						true);
				    sendProgressMessage("Metamodel generated. (" + new Time(durationMillis)+")");
				} else {
				    String name = "metamodelAborted";
				    name = name + "_" + leadingZerosFormat.format(analysisCount++);
				    addAnalysis(new FailedAnalysis(name,
								   textWindow,
								   modelString,
								   commandInfo,
								   startTime,
								   durationMillis),
						true);
				    sendProgressMessage("Metamodel generation aborted.");
				}
			    }
			});
		}
	    };
    }

    /**
     * @param textWindow
     * @param modelString
     * @param commandInfo
     * @param startTime
     * @return
     */
    AlloyController.ThreadFinisher solveFinisher(
						 final ModelPanel textWindow,
						 final String modelString,
						 final Command.Info commandInfo,
						 final Date startTime) {
        return new AlloyController.ThreadFinisher() {
		public void threadFinished(final Object success) {
		    final long durationMillis = System.currentTimeMillis() - startTime.getTime();

		    AlloySwingUtilities.invokeLater(new Runnable() {
			    public void run() {
				boolean solveOk = ((Boolean)success).booleanValue();

				continuouslyUpdateFirstAnalysisRow(false);
				
				StringTokenizer st = new StringTokenizer(commandInfo.toString());
				st.nextToken();
				String commandName = st.nextToken();

				if (solveOk) {
				    boolean isRun = commandInfo.isRunCommand(); // true if run, false if check

				    boolean hasExpect = commandInfo.hasExpects(); //!((FindCommand)commandInfo).getExpects().isEmpty();
				    boolean expectsSol = hasExpect && commandInfo.expectsCount() > 0; //((FindCommand)commandInfo).getExpects().getInt() > 0;

				    if (controller.getInstance() == null) {
					String name = isRun ? "failedRun" : "successfulAssertion";
					name = commandName + "_" + name + "_" + leadingZerosFormat.format(analysisCount++);
					addAnalysis(new FailedAnalysis(name,
								       textWindow,
								       modelString,
								       commandInfo,
								       startTime,
								       durationMillis),
						    true);

					final String expectation =
					    hasExpect ? ", " + (expectsSol ? "contrary to expectation" : "as expected") : "";
					String msg;
					if (isRun) {
					    msg = "No instance found" + expectation + ": " + commandName + " may be inconsistent.";
					} else {
					    msg = "No counterexample found" + expectation + ": " + commandName + " is valid within the specified scope.";
					}
					sendProgressMessage(msg+" ("+new Time(durationMillis)+")");
				    }
				    else {
					String name = isRun ? "instance" : "counterexample";
					name = commandName + "_" + name + "_" + leadingZerosFormat.format(analysisCount++);
					addAnalysis(new SuccessfulAnalysis(name,
									   textWindow,
									   modelString,
									   commandInfo,
									   startTime,
									   durationMillis,
									   controller.getInstance()),
						    true);

					final String expectation =
					    hasExpect ? ", " + (expectsSol ? "as expected" : "contrary to expectation") : "";
					String msg;
					if (isRun) {
					    msg = "Instance found" + expectation + ": " + commandName + " is consistent.";
					} else {
					    msg = "Counterexample found" + expectation + ": " + commandName + " is invalid.";
					}
					sendProgressMessage(msg+" ("+new Time(durationMillis)+")");
				    }
				}
				else {
				    String name = "aborted";
				    name = commandName + "_" + name + "_" + leadingZerosFormat.format(analysisCount++);
				    addAnalysis(new FailedAnalysis(name,
								   textWindow,
								   modelString,
								   commandInfo,
								   startTime,
								   durationMillis),
						true);
				    sendProgressMessage("Execution aborted.");
				}
			    }
			});
		}
	    };
    }

    /**
     * aborts either compilation or execution
     */
    void abort() {
    	AlloyLog.logStartSession(AlloyLog.ABORT);
        sendProgressMessage("Aborting...");
        try {
            controller.abort();
            // System.out.println("just aborted");
        }
        catch (UnavailableOperationException ex) {
            unavailableOperation();
        }
        AlloyLog.logEndSession(AlloyLog.ABORT);
    }

    /** Notify model that data needs to be updated, but don't lose
     *  the previous selection in table if possible.
     *  model must be the TableModel used by table.
     *  Also, stop and restart cell editing in progress,
     *  in order to refresh drop down lists.
     */
    private void updateTableData(final JTable table, final AbstractTableModel model) {
        final int row = table.getSelectedRow();
        model.fireTableDataChanged();
        if (table.getRowCount() > 0) {
            final int newRow = (row >= 0 && row < table.getRowCount()) ? row : table.getRowCount() - 1;
            table.setRowSelectionInterval(newRow, newRow);
        }
    }

    /**
     * @return screen width
     */
    private int getScreenWidth() {
		return AlloySwingUtilities.getScreenWidth();
	}

    /**
	 * @return screen width
	 */
    private int getScreenHeight() {
		return AlloySwingUtilities.getScreenHeight();
	}

    // I have disabled primary relations specification in the GUI for now. -SID
    /**
     * Specify primary relations.  During enumeration, solutions differing only in
     * non-primary relations will be considered the same, so only one of these
     * solutions will be enumerated.  This routine opens a dialogbox that lets
     * the user mark the primary relations.
     */
    /*
    private Set _specifyPrimaryRelations(SolutionData commandData) {
        // ask the user to enter an Alloy instance,
        // rather than asking a solver to find it.
        // the user's instance of course may or may
        // not satisfy the formula.

        PrimaryRelationsDialog primRelDlg = new PrimaryRelationsDialog(mainFrame, commandData);
        primRelDlg.setVisible(true);
        return !primRelDlg.isConfirmed() ? null : primRelDlg.getSelectedLeafIds();
    }
    */
    void unavailableOperation() {
        JOptionPane.showMessageDialog(
				      mainFrame,
				      "That operation is not available",
				      "Error",
				      JOptionPane.ERROR_MESSAGE);
    }

    /* *********************** internal classes ************************ */

    /** An instance of this class is the table model for the main window's upper table,
     *  which lists open files.
     *
     *  FileTableModel uses data stored in variables filePanelList and builtFilePanel.
     */

    class FileTableModel extends AbstractTableModel {
        final String[] columnNames = { FT_MODE,
				       FT_FILENAME,
				       FT_LASTMODIFIED };

        public String getColumnName(final int column) {
            return columnNames[column];
        }

        public Class getColumnClass(final int column) {
        	final String columnName = columnNames[column];
	    if (columnName == FT_LASTMODIFIED)
			return Date.class;
	    else
			return super.getColumnClass(column);
        }

        public int getRowCount() {
            return filePanelList.size();
        }

        public int getColumnCount() {
            return columnNames.length;
        }

        public boolean isCellEditable(int row, int col) {
            return false;
        }

        public Object getValueAt(final int row, final int col) {
            final ModelPanel textWindow = (ModelPanel)filePanelList.get(row);
            final LocatableTextArea textArea = textWindow.getTextArea();
            final String filePath = textArea.getFilePath();

            final String columnName = columnNames[col];
			if (columnName == FT_MODE)
				return textWindow.isEditable() ? "E" : "R";
			else if (columnName == FT_FILENAME)
				return (filePath == null) ? textWindow.getFileString() : filePath;
			else if (columnName == FT_LASTMODIFIED)
				return (filePath == null) ? null : new Date(new File(filePath).lastModified());
			else
				return null;
        }

        public void setValueAt(final Object value, final int row, final int col) {
            if (isCellEditable(row, col))
                fireTableCellUpdated(row, col);
        }
    }

    /**
     *  An instance of this class is the table model for the main window's upper table,
     *  which maintains a history of analyses.
     *
     *  AnalysisTableModel uses data stored in the variable analysisList.
     */
    class AnalysisTableModel extends AbstractTableModel {
    	final String[] columnNames = { AT_TYPE,
				       AT_NAME,
				       AT_FILENAME,
				       AT_COMMAND,
				       AT_TIMESTARTED,
				       AT_ELAPSEDTIME };

    		public String getColumnName(final int column) {
            return columnNames[column];
        }

        public Class getColumnClass(final int column) {
			final String columnName = columnNames[column];
			if (columnName == AT_TYPE)
				return AnalysisIcon.class;
			else if (columnName == AT_TIMESTARTED)
				return Date.class;
			else if (columnName == AT_ELAPSEDTIME)
				return Time.class;
			else
				return super.getColumnClass(column);
        }

        public int getRowCount() {
            return analysisList.size();
        }

        public int getColumnCount() {
            return columnNames.length;
        }

        public boolean isCellEditable(final int row, final int col) {
	    final String columnName = columnNames[col];
		if (columnName == AT_NAME)
			return !(analysisList.get(row) instanceof InProgressAnalysis);
		else
			return false;
        }

        public Object getValueAt(final int row, final int col) {
            final Analysis analysis = (Analysis) analysisList.get(row);

			final String columnName = columnNames[col];
			if (columnName == AT_TYPE) {
				final boolean isRun = analysis._commandInfo.isRunCommand();
		if (analysis instanceof SuccessfulAnalysis) {
					// note by vincent: an alloy.gui.SuccessfulAnalysis is
					// defined in the doc
					// as one that returns an instance, so for a check command,
					// it's one that
					// returns a counterexample, which is a case of a failed
					// assertion.
					return isRun ? AnalysisIcon.SUCCESSFUL_RUN_ICON : AnalysisIcon.FAILED_ASSERTION_ICON;
				} else if (analysis instanceof SuccessfulMetaAnalysis) {
					return AnalysisIcon.META_INSTANCE_ICON;
				} else if (analysis instanceof FailedAnalysis) {
					// note by vincent: an alloy.gui.FailedAnalysis is one that
					// fails to
					// generate an instance, so for a check command, this is
					// indicative of
					//a successful assertion.
					return isRun ? AnalysisIcon.FAILED_RUN_ICON : AnalysisIcon.SUCCESSFUL_ASSERTION_ICON;
				} else if (analysis instanceof InProgressAnalysis) {
					return isRun ? AnalysisIcon.IN_PROGRESS_RUN_ICON : AnalysisIcon.IN_PROGRESS_ASSERTION_ICON;
				} else if (analysis instanceof SuccessfulUnsatCoreAnalysis) {
					return AnalysisIcon.UNSAT_CORE_ICON;
				} else if (analysis instanceof NullAnalysis) {
					return AnalysisIcon.IN_PROGRESS_RUN_ICON;
				} else
					return null;
			} else if (columnName == AT_NAME) {
				return analysis.getName();
			} else if (columnName == AT_FILENAME) {
				return analysis.getFilePanel().getFileString();
			} else if (columnName == AT_COMMAND) {
				if (analysis instanceof SuccessfulMetaAnalysis || analysis instanceof InProgressMetaAnalysis) {
					return "";
				} else {
					return analysis._commandInfo.name == null ? stripAllQualifiers(analysis._commandInfo.toString()) : analysis._commandInfo.name + ": " + analysis._commandInfo.toString();
				}
			} else if (columnName == AT_TIMESTARTED) {
				return analysis.getStartTime();
			} else if (columnName == AT_ELAPSEDTIME) {
				return new Time(analysis.getDurationMillis());
			} else {
				return null;
			}
        }

        public void setValueAt(final Object value, final int row, final int col) {
            final Analysis analysis = (Analysis) analysisList.get(row);

			final String columnName = columnNames[col];
			if (columnName == AT_NAME) {
				analysis.setName((String) value);
			}
        }
    }

    class FileViewerPanel extends AlloyPanel {
        // these menu items must be accessible for enabling/disabling
        private JMenuItem reloadMenuItem;
        private JMenuItem saveMenuItem;
        private JMenuItem saveAsMenuItem;
        private JMenuItem saveCopyAsMenuItem;
        private JMenuItem closeMenuItem;
        private JMenuItem buildMenuItem;
        private JMenuItem executeMenuItem;
        private JMenuItem abortMenuItem;
        private JMenuItem undoMenuItem;
        private JMenuItem redoMenuItem;
        private JMenuItem cutMenuItem;
        private JMenuItem copyMenuItem;
        private JMenuItem pasteMenuItem;
        private JMenuItem deleteMenuItem;

	private JPanel topPanel;
	private JToolBar topToolbar;

	private Component currentFilePanel;
	private JComponent defaultFilePanel;

	FileViewerPanel() {
	    getWindow().setJMenuBar(createMenuBar());
	    topPanel = new JPanel(new BorderLayout());
	    getContentPanel().add(topPanel, BorderLayout.NORTH);

	    getCustomTopBox().add(progressMsgBox);

	    topToolbar = new JToolBar();
	    topToolbar.setBorder(AlloySwingUtilities.createBottomBorder());
	    topPanel.add(topToolbar, BorderLayout.CENTER);
	    topPanel.setVisible(false);

	    defaultFilePanel = new JPanel();
	    if (_onMac())
			defaultFilePanel.setBorder(null);
		else
			defaultFilePanel.setBorder(BorderFactory.createLoweredBevelBorder());
	    previewSelection();

	    addAlloyPanelListener(new AlloyPanelAdapter() {
			public void alloyPanelAttached(final AlloyPanelEvent e) {
				topPanel.setVisible(false);
				topToolbar.remove(modelToolbar);
				progressMsgDash.setVisible(true);
			}

			public void alloyPanelDetached(final AlloyPanelEvent e) {
				progressMsgDash.setVisible(false);
				topToolbar.removeAll();
				topToolbar.add(modelToolbar);
				topPanel.setVisible(true);
			}
		});
	}

	Action tearOffAction() {
	    return new AbstractAction() {
		    public void actionPerformed(ActionEvent e) {
			if (getSelectedFilePanel() != null)
			    getSelectedFilePanel().openTearOff();
			updateAllMenuItems();
		    }
		};
	}
	
	void previewSelection() {
	    if (currentFilePanel != null)
			getContentPanel().remove(currentFilePanel);
		if (fileTable.getSelectedRowCount() == 1) {
			final ModelPanel filePanel = getSelectedFilePanel();
			currentFilePanel = filePanel;
			getContentPanel().add(currentFilePanel, BorderLayout.CENTER);
			setTitle(filePanel.getFileString());
			setTearOffEnabled(filePanel.getTextArea().getFilePath() != null);
		} else {
			currentFilePanel = defaultFilePanel;
			getContentPanel().add(currentFilePanel, BorderLayout.CENTER);
			setTitle("<No File Selected>");
			setTearOffEnabled(false);
		}
	
	    currentFilePanel.setVisible(false);
	    currentFilePanel.setVisible(true);
	    getContentPanel().validate();
	}

        JMenuBar createMenuBar() {
            final JMenuBar mb = new JMenuBar();
			int shortcutKeyMask = AlloySwingUtilities.getShortcutKeyMask();

            // The file menu.
			final JMenu fileMenu = new JMenu("File");
			fileMenu.setMnemonic('F');
			mb.add(fileMenu);

            // And now its contents.
			reloadMenuItem = new JMenuItem("Reload", 'R');
			reloadMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Reload") {
				public void actionPerformed(final ActionEvent e) {
					reloadFile();
				}
			}));
            reloadMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_L, shortcutKeyMask));
            fileMenu.add(reloadMenuItem);

            fileMenu.addSeparator();

            saveMenuItem = new JMenuItem("Save", 'S');
            saveMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Save") {
            		public void actionPerformed(final ActionEvent e) {
            			saveFile();
            		}
            }));
            saveMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_S, shortcutKeyMask));
            fileMenu.add(saveMenuItem);

            saveAsMenuItem = new JMenuItem("Save As...", 'v');
            saveAsMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Save As...") {
		    public void actionPerformed(final ActionEvent e) {
		    		saveFileAs();
		    }
		}));
            fileMenu.add(saveAsMenuItem);

            saveCopyAsMenuItem = new JMenuItem("Save Copy As...", 'C');
            saveCopyAsMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Save Copy As...") {
			public void actionPerformed(final ActionEvent e) {
			    saveFileCopyAs();
			}
		    }));
            fileMenu.add(saveCopyAsMenuItem);

            fileMenu.addSeparator();

            final JMenuItem hideMenuItem = new JMenuItem("Close Window", 'l');
            hideMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Close Window") {
            		public void actionPerformed(final ActionEvent e) {
		    			makeHidden();
		    		}
            }));
            fileMenu.add(hideMenuItem);
            fileMenu.addSeparator();

            closeMenuItem = new JMenuItem("Close File", 'o');
            closeMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Close File") {
		    public void actionPerformed(final ActionEvent e) {
			closeFile();
		    }
		}));
            closeMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_W, shortcutKeyMask));
            fileMenu.add(closeMenuItem);

            // The edit menu.
            final JMenu editMenu = new JMenu("Edit");
            editMenu.setMnemonic('E');
            mb.add(editMenu);

            // ... and it's contents.
            undoMenuItem = new JMenuItem("Undo", 'U');
            undoMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Undo") {
		    public void actionPerformed(final ActionEvent e) {
			getSelectedFilePanel().getTextArea().undo();
		    }
		}));
            undoMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_Z, shortcutKeyMask));
            editMenu.add(undoMenuItem);

            redoMenuItem = new JMenuItem("Redo", 'R');
            redoMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Redo") {
		    public void actionPerformed(final ActionEvent e) {
			getSelectedFilePanel().getTextArea().redo();
		    }
		}));
            redoMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_R, shortcutKeyMask));
            editMenu.add(redoMenuItem);
            editMenu.addSeparator();

            cutMenuItem = new JMenuItem("Cut", 't');
            cutMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Cut") {
		    public void actionPerformed(final ActionEvent e) {
			getSelectedFilePanel().getTextArea().cut();
		    }
		}));
            cutMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_X, shortcutKeyMask));
            editMenu.add(cutMenuItem);

            copyMenuItem = new JMenuItem("Copy", 'C');
            copyMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Copy") {
		    public void actionPerformed(final ActionEvent e) {
			getSelectedFilePanel().getTextArea().copy();
		    }
		}));
            copyMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_C, shortcutKeyMask));
            editMenu.add(copyMenuItem);

            pasteMenuItem = new JMenuItem("Paste", 'P');
            pasteMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Paste") {
		    public void actionPerformed(final ActionEvent e) {
			getSelectedFilePanel().getTextArea().paste();
		    }
		}));
            pasteMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_V, shortcutKeyMask));
            editMenu.add(pasteMenuItem);

            deleteMenuItem = new JMenuItem("Delete", 'D');
            deleteMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Delete") {
		    public void actionPerformed(final ActionEvent e) {
			getSelectedFilePanel().getTextArea().replaceSelection("");
		    }
		}));
            editMenu.add(deleteMenuItem);

            // The tools menu.
            final JMenu toolsMenu = new JMenu("Tools");
            fileMenu.setMnemonic('T');
            mb.add(toolsMenu);

            // And now its contents.
            buildMenuItem = new JMenuItem("Build", 'B');
            buildMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Build") {
		    public void actionPerformed(final ActionEvent e) {
			build(getSelectedFilePanel());
		    }
		}));
            buildMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_B, shortcutKeyMask));
            toolsMenu.add(buildMenuItem);

            executeMenuItem = new JMenuItem("Execute", 'E');
            executeMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Execute") {
		    public void actionPerformed(final ActionEvent e) {
			execute(getSelectedFilePanel());
		    }
		}));
            executeMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_E, shortcutKeyMask));
            toolsMenu.add(executeMenuItem);

            abortMenuItem = new JMenuItem("Abort", 'A');
            abortMenuItem.setAction(AlloySwingUtilities.action(new AbstractAction("Abort") {
		    public void actionPerformed(final ActionEvent e) {
			abort();
		    }
		}));
            abortMenuItem.setAccelerator(KeyStroke.getKeyStroke(KeyEvent.VK_T, shortcutKeyMask));
            toolsMenu.add(abortMenuItem);

            final JMenu windowMenu = AlloyWindow.makeWindowMenu("Window");
            windowMenu.setMnemonic('W');
            mb.add(windowMenu);

            return mb;
        }

        void updateMenuItems() {
        		final boolean fileSelected = (fileTable.getSelectedRowCount() == 1);
			final boolean isBuilt = (fileSelected && builtFilePanel == getSelectedFilePanel());
			final boolean isBuilding = (fileSelected && buildingFilePanel == getSelectedFilePanel());
			final boolean isEditable = (fileSelected && getSelectedFilePanel().isEditable());
			final boolean usePrimRel = false; //Params.glob.getBoolParam("MAIN", "primrel");

			buildMenuItem.setEnabled(fileSelected
					&& (controller == null || controller.isBuildAvailable()));
			executeMenuItem.setEnabled(isBuilt
					&& controller.isExecuteAvailable(usePrimRel));
			abortMenuItem.setEnabled(isBuilding
					&& controller.isAbortAvailable());

	    reloadMenuItem.setEnabled(fileSelected);
	    saveMenuItem.setEnabled(fileSelected && getSelectedFilePanel().isEditable());
	    saveAsMenuItem.setEnabled(fileSelected);
	    saveCopyAsMenuItem.setEnabled(fileSelected);
	    closeMenuItem.setEnabled(fileSelected);

	    undoMenuItem.setEnabled(isEditable);
	    redoMenuItem.setEnabled(isEditable);
	    cutMenuItem.setEnabled(isEditable);
	    copyMenuItem.setEnabled(fileSelected);
	    pasteMenuItem.setEnabled(isEditable);
	    deleteMenuItem.setEnabled(isEditable);
        }
    }

    class InstanceViewerPanel extends AlloyPanel {
	private JPanel outerSettingsPanel;
	private JPanel innerSettingsPanel;

	private Component currentInstancePanel;

	private JPanel currentViewChooser;
	private JPanel defaultViewChooser;

	private JToolBar topToolbar;

	private boolean settingsPanelShown;

	InstanceViewerPanel() {
	    getWindow().setJMenuBar(createMenuBar());

	    topToolbar = new JToolBar();
	    topToolbar.setBorder(AlloySwingUtilities.createBottomBorder());
	    topToolbar.setVisible(false);
	    getContentPanel().add(topToolbar, BorderLayout.NORTH);

	    if (_onMac())
		consolePanel.setBorder(null);
	    else
		consolePanel.setBorder(BorderFactory.createLoweredBevelBorder());
	
	    outerSettingsPanel = new JPanel(new BorderLayout());

	    defaultViewChooser = new JPanel();
	    defaultViewChooser.add(new JLabel("No current visualization"));

	    addAlloyPanelListener(new AlloyPanelAdapter() {
		    public void alloyPanelAttached(final AlloyPanelEvent e) {
			topToolbar.setVisible(false);
			topToolbar.remove(viewsToolbar);

			//viewsToolbarRemoved = false;
			//setupMainToolBarBox();
		    }
		    public void alloyPanelDetached(final AlloyPanelEvent e) {
			//viewsToolbarRemoved = true;
			//setupMainToolBarBox();

			topToolbar.removeAll();
			topToolbar.add(viewsToolbar);
			topToolbar.setVisible(true);
		    }
		});

	    settingsPanelShown = false;

	    previewSelection();
	}

	Action tearOffAction() {
	    return new AbstractAction() {
		    public void actionPerformed(final ActionEvent e) {
			openTearOff();
			updateAllMenuItems();
		    }
		};
	}

	void openTearOff() {
            final AlloyWindow tearOffFrame =
                new AlloyWindow(getSelectedAnalysis().getName() + " (tear-off)");

            tearOffFrame.setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);

	    JComponent mainComponent = null;
	    switch (currentViewMode) {
	    case VIZ_MODE:
		mainComponent = ((VizPanel)currentInstancePanel).getCurrentGraph();
		break;
	    }
	    final JScrollPane scroll = new JScrollPane(mainComponent);
	    if (_onMac()) {
                scroll.setHorizontalScrollBarPolicy(JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
                scroll.setVerticalScrollBarPolicy(JScrollPane.VERTICAL_SCROLLBAR_ALWAYS);
	    }
            tearOffFrame.getContentPane().add(scroll, BorderLayout.CENTER);

            tearOffFrame.setSize(500, 300);
            tearOffFrame.positionNicely();
            tearOffFrame.show();
	}

	void previewSelection() {
	    		if (currentInstancePanel != null)
				getContentPanel().remove(currentInstancePanel);

			if (currentViewChooser != null)
				viewsPanel.remove(currentViewChooser);

			if (analysisTable.getSelectedRowCount() == 1) {
				Analysis analysis = getSelectedAnalysis();
		
		if (analysis instanceof SuccessfulAnalysis) {
		    SuccessfulAnalysis se = (SuccessfulAnalysis)analysis;
		    
                    switch (currentViewMode) {
                    case VIZ_MODE:
                        VizPanel vizPanel = se.getVizPanel();
                        currentInstancePanel = vizPanel;
                        currentViewChooser = vizPanel.makeViewChooser();
                        setTitle(analysis.getName());
                        setTearOffEnabled(true);
                        break;
                    case TREE_MODE:
                        currentInstancePanel = se.getTreeComponent();
                        currentViewChooser = defaultViewChooser;
                        setTitle(analysis.getName());
                        setTearOffEnabled(false);
                        break;
                    case TEXT_MODE:
                        currentInstancePanel = se.getTextComponent();
                        currentViewChooser = defaultViewChooser;
                        setTitle(analysis.getName());
                        setTearOffEnabled(false);
                        break;
                    case XML_MODE:
                    	if (Params.glob.getBoolParam("MAIN","xmlAbbrev")) {
                    		currentInstancePanel = se.getXmlAbbrevTextComponent();
                    	} else {
                        currentInstancePanel = se.getXmlTextComponent();
                    	}
                        currentViewChooser = defaultViewChooser;
                        setTitle(analysis.getName());
                        setTearOffEnabled(false);
                        break;
                    case TABLE_MODE:
                        currentInstancePanel = se.getTableComponent();
                        currentViewChooser = defaultViewChooser;
                        setTitle(analysis.getName());
                        setTearOffEnabled(false);
                        break;
                    case DOT_MODE:
                        currentInstancePanel = se.getDotTextComponent();
                        currentViewChooser = defaultViewChooser;
                        setTitle(analysis.getName());
                        setTearOffEnabled(false);
                        break;
                    case CONSOLE_MODE:
                        currentInstancePanel = consolePanel;
                        currentViewChooser = defaultViewChooser;
                        setTitle("<Messages>");
                        setTearOffEnabled(false);
                        break;
                    }
         } else if (analysis instanceof SuccessfulMetaAnalysis) {
					SuccessfulMetaAnalysis me = (SuccessfulMetaAnalysis) analysis;

					switch (currentViewMode) {
					case VIZ_MODE:
						VizPanel vizPanel = me.getVizPanel();
						currentInstancePanel = vizPanel;
						currentViewChooser = vizPanel.makeViewChooser();
						setTitle(analysis.getName());
						setTearOffEnabled(true);
						break;
					default:
						currentInstancePanel = consolePanel;
						currentViewChooser = defaultViewChooser;
						setTitle("<Messages>");
						setTearOffEnabled(false);
						break;
					}
		} else if (analysis instanceof SuccessfulUnsatCoreAnalysis) {
		    SuccessfulUnsatCoreAnalysis ucore = (SuccessfulUnsatCoreAnalysis)analysis;

		    final LiftedUnsatCoreHighlightVisitor ucoreVisitor = ucore.getLiftedUnsatCoreHighlightVisitor();
		    if(_lastUcoreVisitor != null)
		    		_lastUcoreVisitor.hideLiftedUnsatCore(); //clear the old core markings
		    ucoreVisitor.showLiftedUnsatCore(); //and make the new ones
		    _lastUcoreVisitor = ucoreVisitor; //remember this visitor so we can use it to clear the highlights later
		    
		    currentInstancePanel = consolePanel;
		    currentViewChooser = defaultViewChooser;
		    setTitle("<Messages>");
		    setTearOffEnabled(false);		    
		} else {
					currentInstancePanel = consolePanel;
					currentViewChooser = defaultViewChooser;
					setTitle("<Messages>");
					setTearOffEnabled(false);
				}
			}
            else {
		currentInstancePanel = consolePanel;
		currentViewChooser = defaultViewChooser;
		setTitle("<Messages>");
		setTearOffEnabled(false);
	    }
	    
	    getContentPanel().add(currentInstancePanel, BorderLayout.CENTER);
	    viewsPanel.add(currentViewChooser, BorderLayout.CENTER);
	    currentViewChooser.setVisible(false);
	    currentViewChooser.setVisible(true);
	    viewsPanel.validate();
	    
	    currentInstancePanel.setVisible(false);
	    currentInstancePanel.setVisible(true);
	    getContentPanel().validate();
	    
	    getContentPanel().add(currentInstancePanel, BorderLayout.CENTER);
	    viewsPanel.add(currentViewChooser, BorderLayout.CENTER);
	    currentViewChooser.setVisible(false);
	    currentViewChooser.setVisible(true);
	    viewsPanel.validate();
	    
	    currentInstancePanel.setVisible(false);
	    currentInstancePanel.setVisible(true);
	    getContentPanel().validate();
	    
	    //refreshWindowMenu();
	}
	
	JMenuBar createMenuBar() {
            final JMenuBar mb = new JMenuBar();
            JMenu windowMenu = AlloyWindow.makeWindowMenu("Window");
            windowMenu.setMnemonic('W');
            mb.add(windowMenu);
            return mb;
        }

	// vars used for saving and restoring layout when opening settings
	private JMenuBar menuBar;
	private boolean[] menuWasEnabled;
	private Rectangle restoreBounds;
	private Set windowsToRestore;

	JPanel getSettingsPanel() {
	    return outerSettingsPanel;
	}

	void showSettingsPanel() {
			if (!settingsPanelShown) {
				if (innerSettingsPanel != null)
					outerSettingsPanel.remove(innerSettingsPanel);
				innerSettingsPanel = ((VizPanel) currentInstancePanel)
						.getSettingsPanel();
				outerSettingsPanel.add(innerSettingsPanel, BorderLayout.CENTER);

				// expand panel to fill window
				if (instanceViewerPanel.isAttached()) {
				    /*
				      if (fileViewerPanel.isAttached() &&
				      	fileViewerPanel.isShown()) {
				      	fileViewerPanel.makeHidden();
				      	showFileViewerWhenDone = true;
				      } else {
				      	showFileViewerWhenDone = false;
				      }
				      if (tablePanel.isAttached() &&
				      	tablePanel.isShown()) {
				      	tablePanel.makeHidden();
				      	showTablesWhenDone = true;
				      } else {
				      	showTablesWhenDone = false;
				      }
				    */
					restoreBounds = null;
				} else {
					//showFileViewerWhenDone = false;
					//showTablesWhenDone = false;
					restoreBounds = getWindow().getBounds();
					getWindow().setBounds(new Rectangle(
											(int) (restoreBounds.getX() / 2),
											(int) restoreBounds.getY(),
											(int) (getScreenWidth() - (getScreenWidth() - restoreBounds.getWidth()) / 2),
											(int) restoreBounds.getHeight()));
				}

				// disable menus
				menuBar = isAttached() ? mainFrame.getJMenuBar() : getWindow()
						.getJMenuBar();
				menuWasEnabled = new boolean[menuBar.getMenuCount()];
				for (int i = 0; i < menuBar.getMenuCount(); i++) {
					menuWasEnabled[i] = menuBar.getMenu(i).isEnabled();
					menuBar.getMenu(i).setEnabled(false);
				}

				// hide toolbars
				generalToolbar.setVisible(false);
				modelToolbar.setVisible(false);

				// disable panel buttons
				setTearOffEnabled(false);
				setAttachDetachEnabled(false);
				setHideEnabled(false);

				// hide other windows
				windowsToRestore = new HashSet();
				final Iterator it = AlloyWindow.openWindows().iterator();
				while (it.hasNext()) {
					AlloyWindow window = (AlloyWindow) it.next();
					if ((isAttached() && window != mainFrame) || (!isAttached() && window != getWindow())) {
						window.setVisible(false);
						windowsToRestore.add(window);
					}
				}

				settingsPanelShown = true;
				if (isAttached()) {
					// remember locations
					if (horizontalSplitPane != null) {
						lastHorizontalSplitPaneDivider = horizontalSplitPane.getDividerLocation();
					}
					if (verticalSplitPane != null) {
						lastVerticalSplitPaneDivider = verticalSplitPane.getDividerLocation();
					}
					arrangePanels();
				} else {
					showLeftPanel(getSettingsPanel());
				}
			}
		}

	void hideSettingsPanel() {
	    if (settingsPanelShown) {
		// explicitly fires an update in case settings were changed but "Update" had not been clicked
		updateSettings();
		
		settingsPanelShown = false;
		if (isAttached()) {
		    // remember divider locations
		    if (horizontalSplitPane != null) {
		        lastVizHorizontalSplitPaneDivider = horizontalSplitPane.getDividerLocation();
		    }    
		    arrangePanels();
		} else {		    
		    hideLeftPanel();
		}
		
		// restore panel layout
		//if (showFileViewerWhenDone)
		//fileViewerPanel.makeShown();
		//if (showTablesWhenDone)
		//  tablePanel.makeShown();
		if (restoreBounds != null)
		    getWindow().setBounds(restoreBounds);
		
		// enabled disabled menus
		for (int i=0; i<menuBar.getMenuCount(); i++) {
		    menuBar.getMenu(i).setEnabled(menuWasEnabled[i]);
		}
		
		// unhide toolbars
		generalToolbar.setVisible(true);
		modelToolbar.setVisible(true);
		
		// enable panel buttons
		setTearOffEnabled(true);
		setAttachDetachEnabled(true);
		setHideEnabled(true);
		
		// unhide hidden windows
		final Iterator it = windowsToRestore.iterator();
		while (it.hasNext()) {
		    AlloyWindow window = (AlloyWindow)it.next();
		    window.setVisible(true);
		}
		windowsToRestore = null;
		
			if (isAttached())
				mainFrame.toFront();
			else
				getWindow().toFront();
	    }
	}

	void updateSettings() {
	    ((VizPanel)currentInstancePanel).updateEditor();
	}

		boolean isSettingsPanelShown() {
			return settingsPanelShown;
		}
	}

	private class GUILogPostAsker extends LogPostAsker {
		boolean post;

		public boolean ask(final String msg) {
			final JDialog dialog = new JDialog(mainFrame, "Post Log", true);
			final JPanel mainPanel = new JPanel();
			mainPanel.setLayout(new BoxLayout(mainPanel, BoxLayout.Y_AXIS));

			final ByteArrayOutputStream htmlStream = new ByteArrayOutputStream();
			final PrintStream p = new PrintStream(htmlStream);
			final StringTokenizer t = new StringTokenizer(msg, "\n");

			p.print("<html><center>");
			while (t.hasMoreTokens()) {
				p.print(t.nextToken() + "<br>");
			}
			p.print("</center></html>");

	    final JPanel msgPanel = new JPanel(new BorderLayout());
	    final JLabel msgLabel = new JLabel(htmlStream.toString());
	    msgPanel.add(msgLabel);
	    msgLabel.setHorizontalAlignment(JLabel.CENTER);

	    final JPanel emailPanel = new JPanel();
	    final JTextField emailField = new JTextField(30);
	    emailPanel.add(new JLabel("Email address:"));
	    emailPanel.add(emailField);

	    final JPanel commentPanel = new JPanel();
	    final JTextArea commentArea = new JTextArea(5, 40);
	    commentArea.setLineWrap(true);
	    commentArea.setWrapStyleWord(true);
	    commentPanel.add(new JLabel("Comment:"));
	    commentPanel.add(new JScrollPane(commentArea));

	    final JCheckBox askCheckBox = new JCheckBox("Ask again about posting?", true);
	    final JPanel buttonPanel = new JPanel();
	    final JButton postButton = new JButton();
	    postButton.setAction(AlloySwingUtilities.action(new AbstractAction(
									       "Post via HTTP") {
		    public void actionPerformed(ActionEvent e) {
			post = true;
			if(!askCheckBox.isSelected()) {
                            changeLoggingParam("Always", 
                                               "You've just changed your logging \n" +
                                               "preference to \"Always\": all logs will automatically \n" +
                                               "be posted.  To change this, go into preferences.");
			}
			dialog.dispose();
		    }
    		}));
	    final JButton cancelButton = new JButton();
	    cancelButton.setAction(AlloySwingUtilities.action(new AbstractAction(
										 "Don't Post") {
		    public void actionPerformed(final ActionEvent e) {
			post = false;
			if(!askCheckBox.isSelected()) {
                            changeLoggingParam("Never", 
                                               "You've just changed your logging \n" +
                                               "preference to \"Never\": no log will automatically \n" +
                                               "be posted.  To change this, go into preferences.");
			}
			dialog.dispose();
		    }
    		}));
	    buttonPanel.add(postButton);
	    buttonPanel.add(cancelButton);
	    dialog.getRootPane().setDefaultButton(postButton);

	    mainPanel.add(msgPanel);
	    mainPanel.add(emailPanel);
	    mainPanel.add(commentPanel);
	    mainPanel.add(buttonPanel);
	    mainPanel.add(askCheckBox);

	    dialog.getContentPane().add(mainPanel);
	    dialog.pack();
	    dialog.setLocation((getScreenWidth() - dialog.getWidth()) / 2,
			       (getScreenHeight() - dialog.getHeight()) / 2);
	    dialog.show();

	    AlloyLog.logEmailComment(emailField.getText(),commentArea.getText());

	    return post;
    	}
            
            void changeLoggingParam(String newValue, String message) {
                ParamEditor paramEditor = new ParamEditor(Params.glob);
                //File rcFile = new File(System.getProperty("user.home"), "alloy.cfg");
                Params.glob.setParam("DEVEL", "logging", newValue);
                paramEditor.updateParams();
                try {
                    Params.glob.save(new FileOutputStream(rcFile));
                }
                catch (IOException ex) {
                    JOptionPane.showMessageDialog(
                                                  mainFrame,
                                                  "Error writing file.",
                                                  "Save preferences",
                                                  JOptionPane.ERROR_MESSAGE);
                }
                JOptionPane.showMessageDialog(mainFrame, message);
            }
    }

    class GUIBugPostAsker extends BugPostAsker {
	boolean post;

		public String[] ask(final String msg) {
			final JDialog dialog = new JDialog(mainFrame, "Post Bug", true);
			final JPanel mainPanel = new JPanel();
			mainPanel.setLayout(new BoxLayout(mainPanel, BoxLayout.Y_AXIS));

			final ByteArrayOutputStream htmlStream = new ByteArrayOutputStream();
			final PrintStream p = new PrintStream(htmlStream);
			final StringTokenizer t = new StringTokenizer(msg, "\n");

			p.print("<html><center>");
			while (t.hasMoreTokens()) {
				p.print(t.nextToken() + "<br>");
			}
			p.print("</center></html>");

			final JPanel msgPanel = new JPanel(new BorderLayout());
			final JLabel msgLabel = new JLabel(htmlStream.toString());
			msgPanel.add(msgLabel);
			msgLabel.setHorizontalAlignment(JLabel.CENTER);

			final JPanel emailPanel = new JPanel();
			final JTextField emailField = new JTextField(30);
			emailPanel.add(new JLabel("Email address:"));
			emailPanel.add(emailField);

			final JPanel commentPanel = new JPanel();
			final JTextArea commentArea = new JTextArea(5, 40);
			commentArea.setLineWrap(true);
			commentArea.setWrapStyleWord(true);
			commentPanel.add(new JLabel("Comment:"));
			commentPanel.add(new JScrollPane(commentArea));

			final JPanel buttonPanel = new JPanel();
			final JButton postButton = new JButton();
			postButton.setAction(AlloySwingUtilities.action(new AbstractAction("Post via HTTP") {
				public void actionPerformed(final ActionEvent e) {
					post = true;
					dialog.dispose();
				}
			}));
			final JButton cancelButton = new JButton();
			cancelButton.setAction(AlloySwingUtilities.action(new AbstractAction("Don't Post") {
						public void actionPerformed(final ActionEvent e) {
							post = false;
							dialog.dispose();
						}
					}));
			buttonPanel.add(postButton);
			buttonPanel.add(cancelButton);
			dialog.getRootPane().setDefaultButton(postButton);

			mainPanel.add(msgPanel);
			mainPanel.add(emailPanel);
			mainPanel.add(commentPanel);
			mainPanel.add(buttonPanel);

			dialog.getContentPane().add(mainPanel);
			dialog.pack();
			dialog.setLocation((getScreenWidth() - dialog.getWidth()) / 2,
					(getScreenHeight() - dialog.getHeight()) / 2);
			dialog.show();

			return post ? new String[] { emailField.getText(),
					commentArea.getText() } : null;
		}
	}

	interface FontSetter {
		public void setFont(Font font);
	}

	interface TabSizeSetter {
		public void setTabSize(int tabSize);
	}

	static class Time implements Comparable {
		long _ms;

		Time(final long ms_) {
			_ms = ms_;
		}

		public String toString() {
			final long h = _ms / 3600000;
			final int m = (int) (_ms % 3600000) / 60000;
			final int s = (int) (_ms % 60000) / 1000;
			return (h > 0 ? h + ":" : "") + (m / 10) + (m % 10) + ":"
					+ (s / 10) + (s % 10);
		}

		public int compareTo(final Object o) {
			return new Long(_ms).compareTo(new Long(((Time) o)._ms));
		}
	}

	static Image loadImage(final String pathName) {
		return AlloySwingUtilities.loadImage(pathName);
	}

    /** ********************** main method ************************ */

    public static void main(final String[] argv_) {
        // this needs to be set here or it won't register
        // setting it later doesn't seem to work
        // also, wrapping this statement inside a conditional onMac() 
        // doesn't seem to work either.
        // my conjecture is that it needs to be set before any gui
        // stuff starts happening, and the call to onMac() starts gui
        // stuff ... anyhow, setting this property should be innocuous
        // on other platforms.  -- DFR
        System.setProperty("com.apple.mrj.application.apple.menu.about.name", "Alloy 3.0 (beta)");
        
        Dbg.catchUncaughtExceptions(new Runnable() {
		public void run() {
		    _main(argv_);
		}
	    });
    }

    public static void _main(final String[] argv) {
        Dbg.addArgsToDump(argv);

        final String envCheck = AlloyController.checkEnvironment();
        if (envCheck != null) {
            System.out.println("Alloy Analyzer: " + envCheck);
            System.out.println("Please check your installation.");
            System.out.println("For help, email alloy@mit.edu");
            System.exit(1);
        }

        // work around for bug #4713003, which sometimes causes windows
        // to crash on exit
        System.setProperty("sun.java2d.noddraw", "true");

        // set Mac-specific options
        if (_onMac()) {
            UIManager.put("Label.font", new Font("LucidaGrande", Font.PLAIN, 10));
            UIManager.put("TableHeader.font", new Font("LucidaGrande", Font.PLAIN, 11));
            UIManager.put("ComboBox.font", new Font("LucidaGrande", Font.PLAIN, 11));

            System.setProperty("apple.laf.useScreenMenuBar", "true");
            System.setProperty("apple.awt.showGrowBox", "false");
        }

        final NewAlloyGUI gui = new NewAlloyGUI();
        AlloyLog.logStartSession(AlloyLog.UI);

        if (_onMac()) {
			try {
				Class macUtils = ClassLoader.getSystemClassLoader().loadClass(
						"alloy.gui.mac.MacUtils");
				Method meth = macUtils.getMethod("createApplication",
						new Class[] { NewAlloyGUI.class });
				/*Object macApp =*/ meth.invoke(null, new Object[] { gui });
			} catch (ClassNotFoundException e) {
			} catch (NoSuchMethodException e) {
			} catch (IllegalAccessException e) {
			} catch (java.lang.reflect.InvocationTargetException e) {
			}
		}
    }

    private static boolean _onMac() {
		return AlloySwingUtilities.onMac();
	}


	private AlloySolutionButton makeAlloySolutionButton(
			final String label, final String toolTip, final String imageName, final int MODE) {
		final AlloySolutionButton button = new AlloySolutionButton(label, imageName, MODE);
		button.setToolTipText(toolTip);
		return button;
	}
    
    private class AlloySolutionButton extends AlloyButton {
		public AlloySolutionButton(final String label, final String imageName, final int MODE) {
			setAction(AlloySwingUtilities.action(new AbstractAction(label, new ImageIcon(loadImage(imageName))) {
				public void actionPerformed(ActionEvent e) { setInstanceViewerMode(MODE); }
			}));
		} // end constructor
	} // end class AlloySolutionButton

    private static class AlloySolutionMenuItem extends JRadioButtonMenuItem {
        public final int MODE;
        public AlloySolutionMenuItem(final NewAlloyGUI g, final String label, final int MODE) {
	        super(AlloySwingUtilities.action(new AbstractAction(label) {
		        public void actionPerformed(final ActionEvent e) {
                    // compiler won't let us call this on this, so we have to pass g explicitly
                    // ie, we'd prefer to have this be a non-static inner class, but the compiler's
                    // stupid static check prevents that
		            g.setInstanceViewerMode(MODE);  
		        }
	        }));
            this.MODE = MODE;
        } // end constructor

        /**
         * @param mode
         */
        public void setSelected(final int mode) {
            setSelected(mode == MODE);
        }

    } // end class AlloySolutionMenuItem

}//class NewAlloyGUI



